-
Notifications
You must be signed in to change notification settings - Fork 11
Tutorial FM'19: The Correctness by Construction Approach to Programming
October 7-11, 2019
Porto, Portugal
Registration for the tutorial: https://bit.ly/2JfdBjO
Ina Schaefer [email protected] https://www.tu-braunschweig.de/isf/team/schaefer
Tobias Runge [email protected] https://www.tu-braunschweig.de/isf/team/runge
Loek Cleophas [email protected] https://www.tue.nl/en/research/researchers/loek-cleophas/
Bruce W. Watson [email protected] http://suinformatics.com/staff/
The tutorial will take place on Thursday October 10, 10:30-12:30 (between morning coffee break and lunch break) and 14:00-15:00 (between lunch break and afternoon coffee break).
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,
- Introduction to CbC (Motivation and Foundations)
- Examples step-by-step
- Introduction to the CbC tool
- Advanced CbC and Ongoing Research
- Construction of algorithm taxonomies
- CbC in comparison to post-hoc verification
- Discussion
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