TITLE: An Interactive Way To C
modified: 2019-01-12 19:29
AUTHOR: Musa Al-hassy
EMAIL: alhassy@gmail.com
DESCRIPTION: Learning C program proving using Emacs --reminiscent of Coq proving with Proof General.

filetags: program-proving c emacs frama-c
fileimage: interactive_way_to_c.png 450 450

# +INCLUDE: ~/Dropbox/MyUnicodeSymbols.org
# +INCLUDE: ~/alhassy.github.io/content/MathJaxPreamble.org

▼ Abstract        : noexport : here_only_for_index_html :
  :PROPERTIES:
  :CUSTOM_ID: Abstract
  :END:

# copied from the repo

Do you know what the above program accomplishes?
If you do, did you also spot a special edge case?

We aim to present an approach to program proving in C using a minimal Emacs setup
so that one may produce literate C programs and be able to prove them correct
--or execute them-- using a single button press; moreover the output is again in Emacs.

The goal is to learn program proving using the Frama-C tool
--without necessarily invoking its gui-- by loading the source of this file into
Emacs then editing, executing, & proving as you read along.
One provides for the formal specification of properties of C programs --e.g., using ACSL--
 which can then be verified for the implementations using tools that interpret such annotation
--e.g., Frama-C invoked from within our Emacs setup.

Read on, and perhaps you'll figure out how to solve the missing ~FixMe~ pieces 😉

The intent is for rapid editing and checking.
Indeed, the Frama-c gui does not permit editing in the gui, so one must switch between
their text editor and the gui.
Org mode beginning at the basics is a brief tutorial that covers a lot of Org and,
from the get-go, covers “the absolute minimum you need to know about Emacs!”

If anything, this effort can be construed as a gateway into interactive theorem proving
such as with Isabelle, Coq, or Agda.

The article /aims/ to be self-contained ---not even assuming familiarity with any C!


QUOTE
  The presentation and examples are largely inspired by

  ◦ Gilles Dowek's exquisite text Principles of Programming Languages.
     – It is tremendously accessible!

  ◦ Allan Blanchard's excellent tutorial
    Introduction to C Program Proof using Frama-C and its WP Plugin.

  Another excellent and succinct tutorial is Virgile Prevosto's ACSL Mini-Tutorial.
  In contrast, the tutorial ACSL By Example aims to provide a variety of algorithms
  rendered in ACSL.
QUOTE

There are no solutions since it's too easy to give up and look at the solutions that're
nearby. Moreover, I intend to use some of the exercises for a class I'm teaching ;-)

▼ Content : ignore :

macro: fold #+begin_details
macro: end-fold #+end_details
macro: comment #+begin_comment
macro: end-comment #+end_comment