Tutorial FM'19: The Correctness by Construction Approach to Programming

Runge93 edited this page Dec 10, 2018 · 2 revisions

Symposium on Formal Methods

October 7-11, 2019

Porto, Portugal

Presenters

Ina Schaefer i.schaefer@tu-bs.de https://www.tu-braunschweig.de/isf/team/schaefer

Tobias Runge tobias.runge@tu-bs.de https://www.tu-braunschweig.de/isf/team/runge

Loek Cleophas loek@fastar.org https://www.tue.nl/en/research/researchers/loek-cleophas/

Bruce W. Watson bruce@fastar.org http://suinformatics.com/staff/

Content

Correctness-by-Construction (CbC) is an approach to incrementally create formally correct programs guided by pre- and postcondition specifications. A program is created using refinement rules that guarantee the resulting implementation is correct with respect to the specification.

The CbC approach to program development begins with a Hoare triple comprising a precondition, an abstract statement, and a postcondition. Such a triple should be read as a total correctness assertion, if the precondition holds and its abstract statement “executes” then the execution will terminate and its postcondition will hold. This triple can be refined by using a set of refinement rules, i.e., the statement is replaced by more concrete statements. For example, a loop is introduced, or an abstract statement is replaced by an assignment. If no abstract statement remains, the code is fully specialized.

In the tutorial, we want to introduce participants to the CbC approach to programming. First, we provide the theoretical background of refinement rules. Afterwards, we apply the CbC approach to a series of examples. By using an open source tool, the participants can try the CbC approach on their own. In the end, we present how CbC supports the construction of large-scale algorithmic families, and compare CbC against post-hoc verification.

The purpose of the tutorial is to influence the way the participants approach the task of developing algorithms. Instead of specifying a problem and solving the problem by coding with gut feelings and intuitions, we want to focus on the more formal CbC approach to construct programs. The participants should reflect on their coding style and find their best practice to construct formally correct programs.

The tutorial relies on the following easily accessible text book: Derrick G. Kourie, Bruce W. Watson: The Correctness-by-Construction Approach to Programming. Springer 2012, ISBN 978-3-642-27918-8,

Planned Duration: ½ Day

Agenda:

  1. Introduction to CbC (Motivation and Foundations)
  2. Examples step-by-step
  3. Introduction to the CbC tool
  4. Advanced CbC and Ongoing Research
    1. Construction of algorithm taxonomies
    2. CbC in comparison to post-hoc verification
    3. Discussion

Previous tutorials

At FM 2014 https://www.comp.nus.edu.sg/~pat/FM2014/tutorial.html

At QRS 2017 http://paris.utdallas.edu/qrs17/tutorial_6.html

At CARI/ICTAC 2018 https://www.ictac.org.za/tutorials.html

You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.
Press h to open a hovercard with more details.