Summary – Provable Programming (2ITB0) – 2023
Bugs often occur in software, how to prevent this?
➢ Reduce vulnerability to human errors in development process (review, reduce
complexity, avoid single culture: When you have learned a certain way of doing something, which results
in not thinking about it anymore and hence not really understanding/knowing for sure whether it is the right thing to do
in a certain situation.)
➢ Product approaches
o Testing: testing your product by either simulating it or by actually testing the
product by yourself/ by other users.
o Model checking: a mathematical analysis of your model (so not running a
simulation), which can find mistakes ➔ Very exhaustive.
➢ Source code approaches
o Compiler checks (type checks): the compiler let’s you know that you have
made some type faults either while writing your code or it tells you upon
execution (Python).
o Sanity checks: checking for elementary mistakes. Note: assertions do not
o Assertional verification: Dafny comes into play here. happen at runtime in
Dafny.
Dijkstra’s idea
• Combine source code approach with development process approach
o programmer develops (“derives”) program together with the correctness proof
aka Correctness by Construction (Backhouse, Watson)
• Never really caught on outside a few institutes, why?
o It required disciplined attitude and skilled teachers.
o It required a really good command of logic (predicate calculus).
o It is extremely sensitive to errors
➔ Hence it was dropped
SAT/SMT solvers
• Verify propositional formulas. SAT problem: find true/false values that satisfy a
proposition (theoretically exponential problem, but in practice very efficient).
• And problems translated into them, such as predicate formulas (SMT technique)
• Tremendous increase in power during the last 20 years.
• Application to program verification:
o Problem of errors and problem of discipline were much relieved with this.
o Regarding the need for user’s command of logic: the jury is still out…
What do compilers usually do for us?
• It sees spelling mistakes in comments, but it hardly sees it when it is in code due to
consistency requirement.
• It knows types and can point out type inconsistencies.
• A static type checking compiler checks the written code by relating to the source
code at compile time and proves that it will never occur during the execution of this
program that an other type will be stored into the variable than a value of the type int.
(A statically-typed language is a language where variable types are known at compile
time)
o Type checking applies consistency
, o Static typing is actually the proof of a theorem: all possible executions are
type consistent (type of a value is always consistent with the type of
expression / variable).
• Can we bring the compiler to use for more than just that?
Grand vision: the verifying compiler
• Take type checking to another level: more sophisticated and much broader
specification terms added to the program.
• Tool checks compliance to the provided specification.
• Application: mCRL is a model checking tool developed at the TU/e
o Finds issues such as the race condition underlying the Therac-25 bug
o A question that is raised: who checks the checkers?
➔ An approach to the verifying compiler: Dafny
• Programming language similar to Java and/or csharp
• Specification language
• Verification engine (Z3: an SMT solver)
• It can be considered a verifying compiler.
• Dafny works at the level of the source code.
• Potential of being deployed as a programmer’s tool.
• No special theorem prover skills needed.
• Enhances understanding of the algorithm at hand.
• Command of logic and proofs is still important.
Some simple things can typically be proven by any verifying compiler, such as this:
However, can we prove more complex properties? ➔ With Dafny, we can!
Now, some basic Dafny knowledge you should have:
Note: these happen at the same
time, so x, y := y, x; switches the
current value of x with the current
value of y.
,Let’s talk about Dafny functions.
Note that it uses :int, this
indicates that the functions
returns an integer.
Then, we have the predicates.
These solely can be used in
specifications and not in the
implementations of a specification. NOTE: The “?” symbol is often
used as a convention to
indicate that a predicate has a
So, basically they are functions that Boolean result.
return a Boolean variable.
Partial functions:
, Dafny also uses lemmas.
Lemmas can be used in proofs to help Dafny
verify that the proof actually holds.
Note: technically, a lemma is just a method
Without executable code.
Proof techniques
There are a few different ways to proof something in Dafny.
1. Quantifier introduction
1.1 Forall-introduction
NOTE: The following is equivalent
P(x) => Q(x)
1.2 Exists-introduction
NOTE: The following is equivalent
You have expression E and prove:
Assert P(E) && Q(E)
Bugs often occur in software, how to prevent this?
➢ Reduce vulnerability to human errors in development process (review, reduce
complexity, avoid single culture: When you have learned a certain way of doing something, which results
in not thinking about it anymore and hence not really understanding/knowing for sure whether it is the right thing to do
in a certain situation.)
➢ Product approaches
o Testing: testing your product by either simulating it or by actually testing the
product by yourself/ by other users.
o Model checking: a mathematical analysis of your model (so not running a
simulation), which can find mistakes ➔ Very exhaustive.
➢ Source code approaches
o Compiler checks (type checks): the compiler let’s you know that you have
made some type faults either while writing your code or it tells you upon
execution (Python).
o Sanity checks: checking for elementary mistakes. Note: assertions do not
o Assertional verification: Dafny comes into play here. happen at runtime in
Dafny.
Dijkstra’s idea
• Combine source code approach with development process approach
o programmer develops (“derives”) program together with the correctness proof
aka Correctness by Construction (Backhouse, Watson)
• Never really caught on outside a few institutes, why?
o It required disciplined attitude and skilled teachers.
o It required a really good command of logic (predicate calculus).
o It is extremely sensitive to errors
➔ Hence it was dropped
SAT/SMT solvers
• Verify propositional formulas. SAT problem: find true/false values that satisfy a
proposition (theoretically exponential problem, but in practice very efficient).
• And problems translated into them, such as predicate formulas (SMT technique)
• Tremendous increase in power during the last 20 years.
• Application to program verification:
o Problem of errors and problem of discipline were much relieved with this.
o Regarding the need for user’s command of logic: the jury is still out…
What do compilers usually do for us?
• It sees spelling mistakes in comments, but it hardly sees it when it is in code due to
consistency requirement.
• It knows types and can point out type inconsistencies.
• A static type checking compiler checks the written code by relating to the source
code at compile time and proves that it will never occur during the execution of this
program that an other type will be stored into the variable than a value of the type int.
(A statically-typed language is a language where variable types are known at compile
time)
o Type checking applies consistency
, o Static typing is actually the proof of a theorem: all possible executions are
type consistent (type of a value is always consistent with the type of
expression / variable).
• Can we bring the compiler to use for more than just that?
Grand vision: the verifying compiler
• Take type checking to another level: more sophisticated and much broader
specification terms added to the program.
• Tool checks compliance to the provided specification.
• Application: mCRL is a model checking tool developed at the TU/e
o Finds issues such as the race condition underlying the Therac-25 bug
o A question that is raised: who checks the checkers?
➔ An approach to the verifying compiler: Dafny
• Programming language similar to Java and/or csharp
• Specification language
• Verification engine (Z3: an SMT solver)
• It can be considered a verifying compiler.
• Dafny works at the level of the source code.
• Potential of being deployed as a programmer’s tool.
• No special theorem prover skills needed.
• Enhances understanding of the algorithm at hand.
• Command of logic and proofs is still important.
Some simple things can typically be proven by any verifying compiler, such as this:
However, can we prove more complex properties? ➔ With Dafny, we can!
Now, some basic Dafny knowledge you should have:
Note: these happen at the same
time, so x, y := y, x; switches the
current value of x with the current
value of y.
,Let’s talk about Dafny functions.
Note that it uses :int, this
indicates that the functions
returns an integer.
Then, we have the predicates.
These solely can be used in
specifications and not in the
implementations of a specification. NOTE: The “?” symbol is often
used as a convention to
indicate that a predicate has a
So, basically they are functions that Boolean result.
return a Boolean variable.
Partial functions:
, Dafny also uses lemmas.
Lemmas can be used in proofs to help Dafny
verify that the proof actually holds.
Note: technically, a lemma is just a method
Without executable code.
Proof techniques
There are a few different ways to proof something in Dafny.
1. Quantifier introduction
1.1 Forall-introduction
NOTE: The following is equivalent
P(x) => Q(x)
1.2 Exists-introduction
NOTE: The following is equivalent
You have expression E and prove:
Assert P(E) && Q(E)
