#+TITLE: An Interactive Way To C
#+DATE: <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
* Abstract :noexport:here_only_for_index_html:
:PROPERTIES:...
#+TOC: headlines 2
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!
#+BEGIN_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.
#+END_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
#+toc: headlines 2
#+include: ~/interactive-way-to-c/InteractiveWayToC.org