Functional Programming + Verification
Helmut Seidl | TUM
Summer 2022
Copyright By PowCoder代写 加微信 powcoder
Contents of this lecture
• Correctness of programs
• Functional programming with OCaml
1 Correctness of Programs
• Programmers make mistakes !?
• Programming errors can be expensive, e.g., when a rocket explodes or a vital
business system is down for hours …
• Some systems must not have errors, e.g., control software of planes, signaling
equipment of trains, airbags of cars … Problem
How can it be guaranteed that a program behaves as it should behave?
Approaches
• Careful engineering during software development
• Systematic testing
==⇒ formal process model (Software Engineering) • proof of correctness
==⇒ verification Tool: assertions
1 public class GCD {
2 3 4 5 6 7 8 9
public static void main (String[] args) { intx,y,a,b;
a=read();x=a;
b=read();y=b;
while (x != y)
if (x > y) x = x – y; else y = y – x;
assert(x == y);
} // End of definition of main();
// End of definition of class GCD;
• The static method assert() expects a Boolean argument.
• During normal program execution, every call assert(e); is ignored !?
• If Java is launched with the option: –ea (enable assertions), the calls of assert are evaluated:
⇒ If the argument expression yields true, program execution continues.
⇒ If the argument expression yields false, the error AssertionError is thrown.
The run-time check should evaluate a property of the program state when reaching a particular program point.
The check should by no means change the program state (significantly) !!!
Otherwise, the behavior of the observed system differs from the unobserved system ???
In order to check properties of complicated data-structures, it is recommended to realize distinct inspector classes whose objects allow to inspect the data-structure without interference !
• In general, there are many program executions …
• Validity of assertions can be checked by the Java run-time only for a specific
execution at a time.
We require a general method in order to guarantee that a given assertion is valid …
1.1 Program Verification
Floyd, Stanford U. (1936 – 2001) 9
Simplification
For the moment, we consider MiniJava only:
• only a single static method, namely, main
• only int variables
• only if and while.
• We annotate each program point with an assertion !
• At every program point, we argue that the assertion is valid …
1.2 Background: Logic
Assertion:
“All humans are mortal”,
“Socrates is a human”, “Socrates is mortal”
∀ x. human(x) ⇒ mortal(x) human(Socrates), mortal(Socrates)
If ∀ x. P (x) holds, then also P (a) for a specific a ! If A ⇒ B und A holds, then B must hold as well !
∀x∈Z.x<0 ∨ x=0 ∨ x>0
Deduction: Tautology:
Background: Logic
¬(A∨B) ≡ ¬A∧¬B
¬(A∧B) ≡ ¬A∨¬B
A∧(B ∨C) ≡ (A∧B)∨(A∧C) A∨(B ∧C) ≡ (A∨B)∧(A∨C) A∨(B ∧A) ≡ A
A∧(B∨A) ≡ A
double negation idempotence
De Morgan distributivity absorption
Our Example
x = a = read(); y = b = read();
x != y yes
x < y yes y=y−x;
Discussion
• The program points correspond to the edges of the control-flow diagram !
• We require one assertion per edge ...
Background
d | x holds iff x = d · z for some integer z.
For integers x, y, let gcd(x, y) = 0, if x = y = 0, and the greatest number d which
both divides x and y, otherwise. Then the following laws hold:
Discussion
gcd(x, 0) gcd(x, x) gcd(x, y) gcd(x, y)
= gcd(x, y − x) = gcd(x − y, y)
Idea for the example
• Initially, nothing holds.
• After a=read(); x=a; a = x holds.
• Before entering and during the loop, we should have:
A ≡ gcd(a, b) = gcd(x, y)
• At program exit, we should have:
• These assertions should be locally consistent ...
Our Example
x = a = read();
a=x y = b = read();
x != y yes BA
write(x); no x < y yes
x=x−y; y=y−x;
How can we prove that the assertions are locally consistent?
Sub-problem 1: Assignments
Consider, e.g., the assignment:
In order to have after the assignment: we must have before the assignment:
x > 0, // post-condition y + z > 0. // pre-condition
General Principle
• Every assignment transforms a post-condition B into a minimal assumption that must be valid before the execution so that B is valid after the execution.
• In case of an assignment x = e; the weakest pre-condition is given by WPx = e; (B) ≡ B[e/x]
This means: we simply substitute everywhere in B, x by e !!!
• An arbitrary pre-condition A for a statement s is valid, whenever
A ⇒ WPs (B)
// A implies the weakest pre-condition for B.
assignment:
post-condition:
weakest pre-condition: stronger pre-condition:
even stronger pre-condition:
x − y > 0 x − y > 2 x − y = 3
… in the GCD Program (1):
assignment: x = x-y; post-condition: A weakest pre-condition:
A[x − y/x] ≡ gcd(a,b) = gcd(x − y,y) ≡ gcd(a, b) = gcd(x, y)
… in the GCD Program (2):
assignment: y = y-x; post-condition: A weakest pre-condition:
A[y − x/y] ≡ gcd(a,b) = gcd(x,y − x) ≡ gcd(a, b) = gcd(x, y)
∀ x. B B B[e/x] x = read(); write(e);
WPx = e;(B) WPx = read();(B) WPwrite(e);(B )
≡ B[e/x] ≡ ∀ x. B ≡ B
Discussion
• For all actions, the wrap-up provides the corresponding weakest pre-conditions for a post-condition B.
• An output statement does not change any variable. Therefore, the weakest pre-condition is B itself.
• An input statement x=read(); modifies the variable x unpredictably.
In order B to hold after the input, B must hold for every possible x before the input.
Orientation
x = a = read();
a=x y = b = read();
x != y yes BA
write(x); no x < y yes
x=x−y; y=y−x;
Forthestatements: b=read();y=b; wecalculate:
WPy = b; (A)
≡ gcd(a, b) = gcd(x, b)
WPb = read(); (gcd(a, b) = gcd(x, b))
≡ ∀ b. gcd(a, b) = gcd(x, b) ⇐ a=x
Orientation
x = a = read();
a=x y = b = read();
x != y yes BA
write(x); no x < y yes
x=x−y; y=y−x;
Forthestatements: a=read();x=a; wecalculate: WPx=a;(a=x) ≡ a=a
WPa = read(); (true) ≡ ∀ a. true ≡ true
Sub-problem 2: Conditionals
It should hold:
• A ∧ ¬b ⇒ B0
• A∧b⇒B1 .
This is the case, if A implies the weakest pre-condition of the conditional branching: WPb (B0,B1) ≡ ((¬b) ⇒ B0) ∧ (b ⇒ B1)
The weakest pre-condition can be rewritten into:
WPb (B0,B1) ≡ (b ∨ B0) ∧ (¬b ∨ B1)
≡ (¬b∧B0)∨(b∧B1)∨(B0 ∧B1)
≡ (¬b∧B0)∨(b∧B1)
B0 ≡x>y∧y>0 B1 ≡y>x∧x>0 Assume that b is the condition y > x.
Then the weakest pre-condition is given by:
(x ≥ y ∧ x > y ∧ y > 0) ∨ (y > x ∧ y > x ∧ x > 0) ≡ (x > y ∧ y > 0) ∨ (y > x ∧ x > 0)
≡ x > 0 ∧ y > 0 ∧ x ̸= y
…for the GCD Example
¬b∧A ≡ x≥y∧gcd(a,b)=gcd(x,y)
b∧A ≡ y > x∧gcd(a,b) = gcd(x,y)
==⇒ The weakest pre-condition is given by gcd(a, b) = gcd(x, y)
… i.e., exactly A 32
Orientation
x = a = read();
a=x y = b = read();
x != y yes BA
write(x); no x < y yes
x=x−y; y=y−x;
The argument for the assertion before the loop is analogous:
==⇒ A ≡ (A∧(x = y∨x ̸= y) is the weakest pre- condition for the conditional branching.
b ≡ y̸=x ¬b∧B ≡ A∧x=y
b∧A ≡ A∧x̸=y
Summary of the Approach
• Annotate each program point with an assertion.
• Program start should receive annotation true.
• Verify for each statement s between two assertions A and B, that A
implies the weakest pre-condition of s for B i.e.,
A ⇒ WPs(B)
• Verify for each conditional branching with condition b, whether the assertion A before the condition implies the weakest pre-condition for the post-conditions B0 and B1 of the branching, i.e.,
A ⇒ WPb (B0, B1)
An annotation with the last two properties is called locally consistent. 35
1.3 Correctness
• Which program properties can be verified by means of locally consistent annotations ?
• How can we be sure that our method does not prove wrong claims ??
• In MiniJava, the program state σ consists of a variable assignment, i.e., a mapping of program variables to integers (their values), e.g.,
σ = {x → 5, y → −42}
• A state σ satisfies an assertion A , if
A[σ(x)/x]x∈A
// every variable in A is substituted by its value in σ
is a tautology, i.e., equivalent to true. We write: σ |= A.
A[5/x, 2/y]
= {x→5,y→2} ≡ (x>y)
= {x→5,y→12} ≡ (x>y)
≡ (5 > 12)
A[5/x, 12/y]
Trivial Properties
true false
for every σ for no σ
is equivalent to
σ |= A1 ∧ A2
is equivalent to
σ |= A1 ∨ A2
• An execution trace π traverses a path in the control-flow graph.
• It starts in a program point u0 with an initial state σ0 and leads to a
program point um with a final state σm.
• Every step of the execution trace performs an action and (possibly) changes
program point and state.
==⇒ The trace π can be represented as a sequence
(u0, σ0)s1(u1, σ1) . . . sm(um, σm)
where si are elements of the control-flow graph, i.e., basic statements or
(possibly negated) conditional expressions (guards) … 40
x = a = read(); y = b = read();
5 no x != y yes 2
write(x); 4 no x < y
yes 3 y=y−x;
Assume that we start in point 3 with {x → 6, y → 12}. Then we obtain the following execution trace:
π = (3,{x→6,y→12}) y=y-x; (1,{x → 6,y → 6}) ¬(x != y) (5, {x → 6, y → 6}) write(x); (6,{x → 6,y → 6})
Important operation: Update of of state
σ⊕{x→d} = {z→σz|z̸≡x}∪{x→d}
{x→6,y→12}⊕{y→6} = {x→6,y→6} 42
Assumptions:
Conclusion:
be an execution trace starting in program
• The program points in p are annotated by assertions which are locally consistent.
Let p be a MiniJava program, let π point u and leading to program point v.
• The program point • The program point
is annotated with is annotated with
A, then the final state
If the initial state of π satisfies the assertion
satisfies the assertion B.
• If the start point of the program is annotated with true, then every execution trace reaching program point v satisfies the assertion at v.
• In order to prove that an assertion A holds at a program point v, we require a locally consistent annotation satisfying:
(1) The start point is annotated with true.
(2) The assertion at v implies A.
• So far, our method does not provide any guarantee that v
• If a program point v can be annotated with the assertion cannot be reached.
is ever reached !!! false, then v
Let π = (u0, σ0)s1(u1, σ1) . . . sm(um, σm) Assumption: σ0 |= A.
Proof obligation: σm |= B.
Induction on the length m of the execution trace. Base
The endpoint of the execution equals the startpoint. ==⇒ σ0=σmandA≡B
==⇒ the claim holds.
Important Notion:
Evaluation of Expressions
Program State Arithmetic Expression
Evaluation
σ = {x→5,y→−1,z→21} t ≡ 2∗z+y
tσ = 2∗z+y{x→5,y→ −1,z→21} = 2·21+(−1)
Proposition
For (arithmethic) expressions t, e,
t(σ ⊕ {x → eσ}) = t[e/x]σ
E.g.„ consider t ≡x+y, e ≡2∗z for σ = {x → 5, y → −1, z → 21}.
t (σ ⊕ {x → e σ}) =
= t({x → 42,y → −1,z → 21})
t[e/x] σ =
t(σ⊕{x→42}) = 42+(−1) = 41
(2∗z) +yσ
= (2·21)−1 = 41
Proposition
σ⊕{x→eσ}|=t1
• The square program terminates only for inputs a ≥ 0. • while(true); never terminates.
• Programs without loops terminate always!
Can this example be generalized ??
inti,j,t; t=0;
i = read(); while(i>0){
9 write(t);
j = read();
while (j > 0) { t = t + 1; j = j – 1; } i = i – 1;
• The read number i (if non-negative) indicates how often j is read.
• The total running time (essentially) equals the sum of all non-negative values
read into j
==⇒ the program always terminates !!! 67
Programs with for-loops only of the form: for (i=n; i>0; i–) {…}
// i is not modified in the body
… always terminate !
How can we turn this observation into a method that is applicable to arbitrary loops ?
• Make sure that each loop is executed only finitely often …
• For each loop, identify an indicator value r, that has two properties
(1) r > 0 whenever the loop is entered;
(2) r is decreased during every iteration of the loop.
• Transform the program in a way that, alongside ordinary program execution, the indicator value r is computed.
• Verify that properties (1) and (2) hold!
Eample: Safe GCD Program
inta,b,x,y;
a = read(); b = read(); if(a<0)x=-a;elsex=a; if(b<0)y=-b;elsey=b; if (x == 0) write(y);
else if (y == 0) write(x);
while (x != y)
1 2 3 4 5 6 7 8 9
11 write(x); 12 }
if (y > x) y = y – x; 10 else x = x – y;
We choose: r = x + y Transformation
1 2 3 4 5 6 7 8 9
inta,b,x,y,r;
a = read(); b = read(); if(a<0)x=-a;elsex=a; if(b<0)y=-b;elsey=b; if (x == 0) write(y);
else if (y == 0) write(x);
else { r = x + y; while (x != y) {
if (y > x) y = y – x; 10 else x = x – y;
r = x + y; }
Orientation
a = read(); b = read(); a <0
yes 1 r > 0 x < y yes
r>x+y r=x+y;
3 no write(x);
At program points 1, 2 and 3, we assert:
(1) A ≡ (2) B ≡ (3) true
Then we have:
x ̸= y ∧ x > 0 ∧ y > 0 ∧ r = x + y x>0∧y>0∧r>x+y
A⇒r>0 und B⇒r>x+y
We verify:
WPx!=y(true,A) ≡ x=y ∨ A
⇐ x>0∧y>0∧r=x+y
WPr = x+y;(C)
WPx = x-y;(B) WPy = y-x;(B) WPy>x(…,…)
≡ x>y∧y>0∧r>x
≡ x>0∧y>x∧r>y
≡ (x>y∧y>0∧r>x) ∨
(x > 0 ∧ y > x ∧ r > y)
⇐ x̸=y∧x>0∧y>0∧r=x+y ≡A
Orientation
a = read(); b = read(); a <0
yes 1 r > 0 x < y yes
r>x+y r=x+y;
3 no write(x);
Further propagation of C through the control-flow graph completes the locally consistent annotation with assertions.
We conclude:
• At program points 1 and 2, the assertions r > 0 and r > x+y, respectively, hold.
• During every iteration, r decreases, but stays non-negative.
• Accordingly, the loop can only be iterated finitely often.
==⇒ the program terminates!
General Method
• For every occurring loop while (b) s we introduce a fresh variable r.
• Then we transform the loop into:
assert(r > 0); s;
assert(r > e1); r = e1;
r = e0; while(b) {
for suitable expressions e0, e1.
1.6 Modular Verification and Procedures
Tony Hoare, Microsoft Research, Cambridge 78
• Modularize the correctness proof in a way that sub-proofs for replicated program fragments can be reused.
• Consider statements of the form:
… this means:
If before the execution of program fragment p, assertion execution terminates, then
after execution of p assertion B holds.
A : pre-condition B : post-condition
A holds and program
{x>y} z=x-y; {z>0} {true} if(x<0)x=-x; {x≥0} {x>7} while(x!=0)x=x-1; {x=0} {true} while(true); {false}
Modular verification can be used to prove the correctness of programs using functions/methods.
Simplification
We only consider
• procedures, i.e., static methods without return values;
• global variables, i.e., all variables are static as well.
// will be generalized later
1 int a, b;
2 int x, y;
4 void main () {
a = read();
b = read();
write (x – y);
void mm() { if(a> b) {
y= a; x= b;
y= b; } else {
• for simplicity, we have removed all qualifiers static.
• The procedure definitions are not recursive.
• The program reads two numbers.
• The procedure minmax stores the larger number in x, and the smaller number in y.
• The difference of x and y is returned.
• Our goal is to prove:
{a ≥ b} mm(); {a = x}
• For every procedure f(), we provide a
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com