#+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

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

* Abstract        :noexport:here_only_for_index_html:

#+TOC: headlines 2

# 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!

  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.

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