CS代写 Functional Programming

Functional Programming
Verification
Winter 2018/19

Institute of Informatics TU München

Contents of this lecture
• Correctness of programs
• Functional programming with OCaml

Web page: tum.twbk.de 3

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 …
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

public class GCD {
public static void main (String[] args) {
int x, 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)

Simplification
For the moment, we consider MiniJava only:
• only a single static method, namely, main
• only int variables
• only if and while.

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 …

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 a formula !
• At every program point, we prove that the assertion is valid

Background: Logic
Assertion:
“All humans are mortal”, “Socrates is a human”,
Deduction:
Tautology:
“Socrates is mortal”

Background: Logic
Assertion:
“All humans are mortal”,
“Socrates is a human”, “Socrates is mortal”
∀ x. human(x) ⇒ mortal(x) human(Socrates), mortal(Socrates)
Deduction:
Tautology:

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 !
Deduction:
Tautology:

Background:
Logic (cont.)
A ∧ A ≡ A A∨A≡A
¬(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();

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:

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:

Our Example
x = a = read();
a=x y = b = read();
x != y yes BA
write(x); no x < y yes 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.

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
WP[[x = e;]] (B) ≡ B[e/x]
This means: we simply substitute everywhere in B, x by e !!!

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);
WP[[;]](B) ≡ B WP[[x = e;]](B) ≡ B[e/x] WP[[x = read();]](B) ≡ ∀x.B WP[[write(e);]](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 For the statements: b = read(); y = b; we calculate: WP[[y = b;]] (A) ≡ A[b/y] ≡ gcd(a, b) = gcd(x, b) For the statements: b = read(); y = b; we calculate: WP[[y = b;]] (A) ≡ A[b/y] ≡ gcd(a, b) = gcd(x, b) WP[[b = read();]] (gcd(a, b) = gcd(x, b)) ≡ ∀ b. gcd(a, b) = gcd(x, b) Orientation x = a = read(); a=x y = b = read(); x != y yes BA write(x); no x < y yes For the statements: a = read(); x = a; we calculate: WP[[x = a;]](a=x) ≡ a=a ≡ true WP[[a = read();]] (true) ≡ ∀ a. true ≡ true Sub-problem 2: Conditionals A It should hold: A ∧ ¬b ⇒ B0 and A∧b⇒B1 . This is the case, if A implies the weakest pre-condition of the conditional branching: WP[[b]] (B0, B1) ≡ ((¬b) ⇒ B0) ∧ (b ⇒ B1) Die schwächste Vorbedingung können wir umschreiben in: This is the case, if A implies the weakest pre-condition of the conditional branching: WP[[b]] (B0, B1) ≡ ((¬b) ⇒ B0) ∧ (b ⇒ B1) The weakest pre-condition can be rewritten into: WP[[b]] (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:

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 45

… for the GCD Example
¬b∧A ≡ x≥y∧gcd(a,b)=gcd(x,y)
b∧A ≡ y>x∧gcd(a,b)=gcd(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

Orientation
x = a = read();
a=x y = b = read();
x != y yes BA
write(x); no x < y yes The argument for the assertion before the loop is analogous: b ≡ y̸=x ¬b∧B ≡ B b∧A ≡ A∧x̸=y ==⇒ A ≡ (A ∧ x = y) ∨ (A ∧ x ̸= y) is the weakest pre- condition for the conditional branching. 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 ⇒ WP[[s]](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 ⇒ WP[[b]] (B0, B1) An annotation with the last two properties is called locally consistent. 1.2 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} • 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)

σ = A ≡ A[5/x, 2/y] ≡
σ = A ≡ A[5/x, 12/y] ≡
{x􏰀→5,y􏰀→2} (x>y)
{x􏰀→5,y􏰀→12} (x>y)

• 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 conditions (guards) …

x = a = read(); y = b = read();
5 no x != y yes 2
write(x); 4 no x < y yes 3 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}) Let p be a MiniJava program, let π be an execution trace starting in program point u and leading to program point v. Assumptions: • The program points in are locally consistent. • The program point u • The program point v p are annotated by assertions which is annotated with A. is annotated with B. Let p be a MiniJava program, let π be an execution trace starting in program point u and leading to program point v. Assumptions: • The program points in are locally consistent. p are annotated by assertions which • The program point • The program point Conclusion: If the initial state of π state satisfies the assertion B. is annotated with is annotated with A, then the final satisfies the assertion • 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. • 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 is ever reached !!! • If a program point v can be annotated with the assertion false, then v cannot be reached. Let π = (u0,σ0)s1(u1,σ1) . . . sm(um,σm) Assume: σ0 |= A. Proof obligation: σm |= B. Idea Induction on the length m of the execution trace. der Ausführung ist gleich dem Startpunkt. ==⇒ σ0=σmundA≡B ==⇒ Behauptung gilt. Conclusion • The method of Floyd allows us to prove that an assertion B holds whenever (or under certain assumptions) a program point is reached ... • For the implementation, we require: • the assertion true at the start point • assertions for each further program point • a proof that the assertions are locally consistent ==⇒ Logic, automated theorem proving 1.3 Optimization Goal: Reduction of the number of required assertions Observation If the program has no loops, a weakest pre-condition can be calculated for each program point !!! Example (cont.) Assume B≡z=i2 ∧ x=2i−1 Then we calculate: B1 ≡ WP[[i = i+1;]](B) ≡ z = (i+1)2 ∧x = 2(i+1)−1 ≡ z=(i+1)2 ∧x=2i+1 Example (cont.) Assume B≡z=i2 ∧ x=2i−1 Then we calculate: B1 ≡ WP[[i = i+1;]](B) B2 ≡ WP[[z = z+x;]](B1) ≡ z = (i+1)2 ∧x = 2(i+1)−1 ≡ z=(i+1)2 ∧x=2i+1 ≡ z+x = (i+1)2 ∧x = 2i+1 ≡ z=i2∧x=2i+1 Example (cont.) Assume B≡z=i2 ∧ x=2i−1 Then we calculate: B1 ≡ WP[[i = i+1;]](B) B2 ≡ WP[[z = z+x;]](B1) B3 ≡ WP[[x = x+2;]](B2) ≡ z = (i+1)2 ∧x = 2(i+1)−1 ≡ z=(i+1)2∧x=2i+1 ≡ z+x = (i+1)2 ∧x = 2i+1 ≡ z=i2∧x=2i+1 ≡ z=i2 ∧x+2=2i+1 ≡ z=i2∧x=2i−1 ≡B • For every loop, select one program point. Meaningful selections: → Before the condition → At the entry of the loop body → At the exit of the loop body ... • Provide an assertion for each selected program point ==⇒ loop invariant • For all other program points, the assertions are obtained by means of WP[[...]](). int a, i, x, z; a = read(); while (i != a) { } assert(z==a*a); write(z); a = read(); write(z); Stop We verify: WP[[i != a]](z = a2, B) ≡ (i=a∧z=a2) ∨ (i̸=a∧B) ≡ (i=a∧z=a2) ∨ (i̸=a∧z=i2 ∧x=2i−1) ⇐ (i̸=a∧z=i2 ∧x=2i−1) ∨ (i=a∧z=i2 ∧x=2i−1) ≡ z=i2∧x=2i−1 ≡ B Orientation a = read(); write(z); Stop We verify: WP[[z = 0;]](B) WP[[x = -1;]](i=0∧x=−1) WP[[i = 0;]](i = 0) WP[[a = read();]](true) ≡ 0=i2∧x=2i−1 ≡ i=0∧x=−1 1.4 Termination • By our approach, we can only prove that an assertion is valid at a program point whenever that program point is reached !!! • How can we guarantee that a program always terminates ? • How can we determine a sufficient condition which guarantees termination of the program ?? • The GCD program only terminates for inputs a, b with a = b or a > 0 and b > 0.
• The square program terminates only for inputs a ≥ 0. • while (true) ; never terminates.
• Programs without loops terminate always!

• The GCD program only terminates for inputs a, b with a = b or a > 0 and b > 0.
• The square program terminates only for inputs a ≥ 0. • while (true) ; never terminates.
• Programs without loops terminate always!
Can this example be generalized ??

int i, j, t;
i = read();
while (i>0) {
j = read();
while (j>0) { t = t+1; j = j-1; }
} write(t);
• 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

Programs with for-loops only of the form: for (i=n; i>0; i–) {…}
// i is not modified in the body
… always terminate !

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!

Safe GCD Program
int a, b, x, y;
a = read(); b = read();
if (a < 0) x = -a; else x = a; if (b < 0) y = -b; else y = b; if (x == 0) write(y); else if (y == 0) write(x); while (x != y) if (y > x) y = y-x;
else x = x-y;

We choose: r = x + y Transformation
int a, b, x, y, r;
a = read(); b = read();
if (a < 0) x = -a; else x = a; if (b < 0) y = -b; else y = b; if (x == 0) write(y); else if (y == 0) 程序代写 CS代考加微信: powcoder QQ: 1823890830 Email: powcoder@163.com

Related Posts