Course Introduction Program, Solution Specification Elementary programs Structures Deduction Recursion Tools
Programming methodology
Proving correctness of algorithms
Gergely Feldhoffer
Gergely Feldhoffer Programming methodology
Course Introduction Program, Solution Specification Elementary programs Structures Deduction Recursion Tools
Overview of the course topic
Correctness of algorithms
Proof of correctness
Method to prove correctness
Proofs for basic algorithms
Some practical tools at the end of the semester concerning
software correctness (gdb, valgrind)
Gergely Feldhoffer Programming methodology
Course Introduction Program, Solution Specification Elementary programs Structures Deduction Recursion Tools
Course material
This material is originated from Dijsktra and Hoare using
advanced mathematical toolkit as temporal logic
We will discuss the same terms defined with basic set theory
This model was created by Ákos Fóthi using Hungarian
definitions
→ so be prepared, there are no English sources but this
presentation
Gergely Feldhoffer Programming methodology
Course Introduction Program, Solution Specification Elementary programs Structures Deduction Recursion Tools
What to do for your grade
At end of October or at the beginning of November you will
write a test. The possible outcomes are
You are awarded with the best grade without taking the exam
You can attend to the exam
You have to write the test again at the last week
At the exam you have to convince me about the clarity of
your understanding of the theory of algorithm proving.
Gergely Feldhoffer Programming methodology
Course Introduction Program, Solution Specification Elementary programs Structures Deduction Recursion Tools
Sets State space Strings
Relations
You should be familiar with the terms of set, element, ∅,
direct multiplication A × B, elementary tuple (x, y ) ∈ A × B,
relation F ⊆ A × B, set size |A|
DF = {∀x : F (x) 6= ∅} is the domain of the relation F
RF = {∀y : ∃x : F (x) = y } is the range of the relation F
An F relation is function if ∀x ∈ DF : |F (X )| = 1
Gergely Feldhoffer Programming methodology
Course Introduction Program, Solution Specification Elementary programs Structures Deduction Recursion Tools
Sets State space Strings
State space
Def: State space
Let A1 , A2 , . . . , An finite or countably infinite not empty sets. In
this case A = A1 × A2 × . . . × An is called state space, and Ai are
type value sets.
Gergely Feldhoffer Programming methodology
Course Introduction Program, Solution Specification Elementary programs Structures Deduction Recursion Tools
Sets State space Strings
Strings
Let A be a set. We call all possible finite strings of A as A∗ .
This operator is the Kleene star.
If α ∈ A∗ then the elements of the string can be expressed like
α1 , α2 , . . . , α|α|
The last element of the string can be also expressed like τ (α)
A∞ is all possible infinite strings on set A.
We will use A∗∗ = A∗ ∪ A∞ for all finite and infinite string on
set A
The function τ is not defined on infinite strings.
The reduction of a string is a process where every finite direct
recurrences of the same elements are replaced with only one
element, like red(h12333445i) = h12345i
Gergely Feldhoffer Programming methodology
Course Introduction Program, Solution Specification Elementary programs Structures Deduction Recursion Tools
Problem Program Program function Solution
Problem
Def.: Problem
We will call F ⊆ A × A relation a problem on state space A
For a starting state a ∈ A the possible valid solutions are the set
F (a).
A relation is deterministic if ∀a ∈ A : |F (a)| ≤ 1
If a problem does not assign anything to an a ∈ A that means
that there are no demands for this starting state. A possible
misunderstanding would be to think that there are no valid
answers for the state, but we will use this state in quite an
opposite way, so F (a) = ∅ and F (a) = A are equivalent in
some way.
Gergely Feldhoffer Programming methodology
Course Introduction Program, Solution Specification Elementary programs Structures Deduction Recursion Tools
Problem Program Program function Solution
Program
Def.: Program
S ⊆ A × A∗∗ is program if
1 DS = A
2 ∀a ∈ A : ∀α ∈ S(a) : α1 = a
3 ∀α ∈ RS : α = red(α)
The strings of states are the temporal stages of the machine
as the program runs. Different starting states can mean
different input values.
The program has to start from every state
The program must start in the starting state
In each step something has to happen
Gergely Feldhoffer Programming methodology
Course Introduction Program, Solution Specification Elementary programs Structures Deduction Recursion Tools
Problem Program Program function Solution
Program and variables
Def: Variable
Let A = A1 × A2 × . . . × An be a state space. In this case for each
i ∈ [1 . . . n] : fi ⊆ A × Ai = {x ∈ A : fi (x) = projAi (x)}
So the variable is not a single one dimensional subspace of the
state space but the projection function to it. The subspace is the
set containing the possible elements eg. integer numbers. The
variable is more than a set, it has history as the program runs. For
each S(a) a projection of this string is how the given variable
changes its value.
Gergely Feldhoffer Programming methodology
Course Introduction Program, Solution Specification Elementary programs Structures Deduction Recursion Tools
Problem Program Program function Solution
Program function
Def.: Program function
If S ⊆ A × A∗∗ is program then we will define p(S) ⊆ A × A
program function of S as
1 Dp(S) = {a ∈ A : S(a) ⊆ A∗ }
2 ∀a ∈ Dp(S) : p(S)(a) = {b ∈ A : ∃a ∈ S(a) : b = τ (a)}
So the program function is defined only where the program
certainly terminates,
and assigns to starting state a the set of the possible
outcomes of that state a at the end of the program run.
Gergely Feldhoffer Programming methodology
Course Introduction Program, Solution Specification Elementary programs Structures Deduction Recursion Tools
Problem Program Program function Solution
Solution
Def.: Solution
An S ⊆ A × A∗∗ program solves the problem F if
1 DF ⊆ Dp(S)
2 ∀a ∈ DF : p(S)(a) ⊆ F (a)
So the program should certainly terminate where there are
any demands for a starting state,
and for each starting state the set of possible outcomes of the
program run must be ones of the valid outcomes.
if the program is deterministic then this can be expressed as
p(S)(a) ∈ F (a), and if both the program and the problem is
deterministic, then p(S)(a) = F (a)
Gergely Feldhoffer Programming methodology
Course Introduction Program, Solution Specification Elementary programs Structures Deduction Recursion Tools
Precondition, postcondition Weakest precondition Parameter space Specification Example
Truth set
If R ⊆ A × L then
Truth set of R :
dRe = {a ∈ A : R(A) = {true}}
Weak truth set of R :
bRc = {a ∈ A : true ∈ R(A)}
Note that if R is function then dRe = bRc
Q → R ⇒ dQe ⊆ dRe
Gergely Feldhoffer Programming methodology
Course Introduction Program, Solution Specification Elementary programs Structures Deduction Recursion Tools
Precondition, postcondition Weakest precondition Parameter space Specification Example
Precondition, postcondition
We will use the term precondition as a condition which is
true for all starting state of the state space where we have
demand for the output, and the
postcondition which is true for all valid input-output pairs
and false for everything else.
If S ⊆ A × A∗∗ is a program any R ⊆ A × L condition on
state space A can be used as precondition or postcondition
Our goal is to express the problem using only precondition and
postcondition.
Gergely Feldhoffer Programming methodology
Course Introduction Program, Solution Specification Elementary programs Structures Deduction Recursion Tools
Precondition, postcondition Weakest precondition Parameter space Specification Example
Weakest precondition
Def: Weakest precondition
S ⊆ A × A∗∗ is a program, R ⊆ A × L is a condition. R is the
weakest precondition of S if
dwp(S, R)e = {a ∈ Dp(S) : p(S)(a) ⊆ dRe}
So which is the section of the state space where if we run S
program, we will certainly arrive in states where R is true.
Gergely Feldhoffer Programming methodology
Course Introduction Program, Solution Specification Elementary programs Structures Deduction Recursion Tools
Precondition, postcondition Weakest precondition Parameter space Specification Example
Properties of weakest precondition
Let S ⊆ A × A∗∗ be a program, and Q, R ⊆ A × L,
then
Principle ’Exclusion of miracles’: wp(S, False) = False where
False ⊆ A × L = ∀a ∈ A : False(a) = false
Monotonicity: If Q ⇒ R then wp(S, Q) ⇒ wp(S, R)
wp(S, Q) ∧ wp(S, R) = wp(S, Q ∧ R)
wp(S, Q) ∨ wp(S, R) = wp(S, Q ∨ R)
Gergely Feldhoffer Programming methodology
Course Introduction Program, Solution Specification Elementary programs Structures Deduction Recursion Tools
Precondition, postcondition Weakest precondition Parameter space Specification Example
Parameter space
Def: Parameter space
Let F ⊆ A × A problem. We name set B parameter space of F if
∃F1 , F2 : F1 ⊆ A × B ∧ F2 ⊆ B × A ∧ F = F2 ◦ F1
where R1 ◦ R2 is composition of relations meaning if
a ∈ (R1 ◦ R2 )(b) then a ∈ R1 (R2 (b))
note that the order of arguments of expression R1 ◦ R2 and the
order of evaluation is opposite.
The parameter space can be subspace of the state space, restricting
to the input variables. This will be our choice from now on,
however, this definition allows to use even the whole state space.
Gergely Feldhoffer Programming methodology
Course Introduction Program, Solution Specification Elementary programs Structures Deduction Recursion Tools
Precondition, postcondition Weakest precondition Parameter space Specification Example
Specification
Theorem: Theorem of Specification
Let F ⊆ A × A problem, B is a parameter space of F ,
F1 ⊆ A × B ∧ F2 ⊆ B × A ∧ F = F2 ◦ F1 , and b ∈ B
dQb e = {a ∈ A : (a, b) ∈ F1 } = inv (F1 )(b)
dRb e = {a ∈ A : (b, a) ∈ F2 } = F2 (b)
In this case if ∀b ∈ B : Qb ⇒ wp(S, Rb ) then program S solves
problem F
Which means if we can express our demands with precondition and
postcondition, then we defined a problem, and we also give a
possible method to check whether a program is a solution or not.
Gergely Feldhoffer Programming methodology
Course Introduction Program, Solution Specification Elementary programs Structures Deduction Recursion Tools
Precondition, postcondition Weakest precondition Parameter space Specification Example
Proof of theorem of specification
Let F ⊆ A × A problem, B is a parameter space of F ,
F1 ⊆ A × B ∧ F2 ⊆ B × A ∧ F = F2 ◦ F1 , and b ∈ B
dQb e = {a ∈ A : (a, b) ∈ F1 } = inv (F1 )(b)
dRb e = {a ∈ A : (b, a) ∈ F2 } = F2 (b)
In this case if ∀b ∈ B : Qb ⇒ wp(S, Rb ) then program S solves
problem F
Proof:
DF ⊆ Dp(S) since every a ∈ DF : ∃b ∈ B : a ∈ dQb e because
of F1 . Since Qb ⇒ wp(S, Rb ) so
a ∈ dQb e ⊆ dwp(S, Rb )e ⊆ (D)p(S)
∀a ∈ DF : p(S)(a) ⊆ F (a) since if a ∈ DF and
b ∈ B ∧ a ∈ dQb e then
p(S)(a) ⊆ dRb e = F2 (b) ⊆ F2 (F1 (a)) = F (a)
Gergely Feldhoffer Programming methodology
Course Introduction Program, Solution Specification Elementary programs Structures Deduction Recursion Tools
Precondition, postcondition Weakest precondition Parameter space Specification Example
Example of specification
Example: addition of two numbers
A = Zx × Zy × Zz
B = Zx 0 × Zy 0
Qx 0 (b),y 0 (b) (a) = (x(a) = x 0 (b) ∧ y (a) = y 0 (b))
Rx 0 (b),y 0 (b) (a) = (x(a) = x 0 (b)∧y (a) = y 0 (b)∧z(a) = x 0 (b)+y 0 (b))
We will use x 0 and y 0 are represent the starting value of the
variable as it is in the parameter space.
This formalism can be simplified since each raw variable is defined
on A and each parameter is defined on B ..
Gergely Feldhoffer Programming methodology
Course Introduction Program, Solution Specification Elementary programs Structures Deduction Recursion Tools
Precondition, postcondition Weakest precondition Parameter space Specification Example
Example of specification
Example: addition of two numbers
A = Zx × Zy × Zz
B = Zx 0 × Zy 0
Qx 0 ,y 0 (a) = (x = x 0 ∧ y = y 0 )
Rx 0 ,y 0 (a) = (x = x 0 ∧ y = y 0 ∧ z = x 0 + y 0 )
..and since Q and R has to be defined on the whole parameter
space..
Gergely Feldhoffer Programming methodology
Course Introduction Program, Solution Specification Elementary programs Structures Deduction Recursion Tools
Precondition, postcondition Weakest precondition Parameter space Specification Example
Example of specification
Example: addition of two numbers
A = Zx × Zy × Zz
B = Zx 0 × Zy 0
Q : x = x0 ∧ y = y0
R : x = x0 ∧ y = y0 ∧ z = x0 + y0
..we arrived to the formalism we will use for specifications.
Gergely Feldhoffer Programming methodology
Course Introduction Program, Solution Specification Elementary programs Structures Deduction Recursion Tools
Elementary program Skip Abort Assignment Program functions
Elementary program
Elementary program
S ⊆ A × A∗∗ program is elementary if
∀a ∈ A : ∀α ∈ S(a) : (∃b ∈ A : α = red(habi)) ∨ α = haa . . .i
So a program is elementary if it does exactly one step or hangs.
We will use some special elementary programs such as SKIP,
ABORT, and assignment.
Gergely Feldhoffer Programming methodology
Course Introduction Program, Solution Specification Elementary programs Structures Deduction Recursion Tools
Elementary program Skip Abort Assignment Program functions
Skip Abort
SKIP
SKIP = {(a, α) ∈ A × A∗∗ : α = hai}
ABORT
ABORT = {(a, α) ∈ A × A∗∗ : α = haaa . . .i}
Gergely Feldhoffer Programming methodology
Course Introduction Program, Solution Specification Elementary programs Structures Deduction Recursion Tools
Elementary program Skip Abort Assignment Program functions
Assignment
Every other elementary programs are general assignments. To
handle assignments, we will use a state transition function E to
describe it: E ⊆ A × A, so if we are in state a we step to (one of
the) state(s) E (a).
So if we have an E as DE = A, then
SE = {(a, α) ∈ A × A∗∗ : α = red(habi) : b ∈ E (a)}
Gergely Feldhoffer Programming methodology
Course Introduction Program, Solution Specification Elementary programs Structures Deduction Recursion Tools
Elementary program Skip Abort Assignment Program functions
Assignment
In general DE = A is not true, in these cases where the state
transition function is not defined, the assignment should abort.
Assignment
SE = {(a, α) ∈ A × A∗∗ : a ∈ DE ∧ α = red(habi) ∧ b ∈ E (a)}∪
∪{(a, α) ∈ A × A∗∗ : a ∈
/ DE ∧ α = haaa . . .i}
Note that every state transition can be an assignment. Each
machine support a limited possibilities of state transitions, that is
why we can not solve NP complete tasks in one step.
Computer science calls esoteric imaginary state transitions as
oracle. Interestingly it is proven that on a machine which supports
every usual operation and includes one NP complete task, on that
machine P=NP. The hard part is to prove that NP on this machine
is not stronger.
Gergely Feldhoffer Programming methodology
Course Introduction Program, Solution Specification Elementary programs Structures Deduction Recursion Tools
Elementary program Skip Abort Assignment Program functions
Program functions of elementary programs
wp(SKIP, R) = R
wp(ABORT , R) = False
wp(SE , R) = {a ∈ DE : E (a) ⊆ dRe}
Dp(SKIP) = A
∀a ∈ A : p(SKIP)(a) = a
Dp(ABORT ) = ∅
p(SE ) = E
Gergely Feldhoffer Programming methodology
Course Introduction Program, Solution Specification Elementary programs Structures Deduction Recursion Tools
Elementary program Skip Abort Assignment Program functions
Notations
Example: A = Zx × Zy
E = {(a, b) ∈ A × A : y (b) = 2 ∗ x(a) ∧ x(b) = x(a)}
We will be noted as y := 2x, this is a simple assignment
E = {(a, b) ∈ A × A : y (b) = 2 ∗ x(a) ∧ x(b) = x(a) + 1}
as x, y := x + 1, 2x, this is a parallel assignment
E = {(a, b) ∈ A × A : y (b) ∈ X }
as y :∈ X , this is a value choice
Gergely Feldhoffer Programming methodology
Course Introduction Program, Solution Specification Elementary programs Structures Deduction Recursion Tools
Sequence Branch Loop Program functions of program structures
Program structures
We will use three kind of program structure: sequence, branch, and
loop.
The sequence means running two program after each other. The
branch means state dependent conditional program execution. The
loop is state dependent repeated execution of a program.
Note that every program can be used as part of program structure.
Every usage of a program structure results a program.
Gergely Feldhoffer Programming methodology
Course Introduction Program, Solution Specification Elementary programs Structures Deduction Recursion Tools
Sequence Branch Loop Program functions of program structures
Sequence
Def: Sequence
Let S1 , S2 ⊆ A × A∗∗ be programs. We will call S ⊆ A × A∗∗ as
Sequence of S1 and S2 if ∀a ∈ A :
S(a) = {α ∈ A∞ : α ∈ S1 (a)}∪
∪{red(concat(α, β)) ∈ A∗∗ : α ∈ S1 (a) ∩ A∗ ∧ β ∈ S2 (τ (α))}
Gergely Feldhoffer Programming methodology
Course Introduction Program, Solution Specification Elementary programs Structures Deduction Recursion Tools
Sequence Branch Loop Program functions of program structures
Branch
Def: Branch
Let π1 , . . . , πn : A → L be conditions, S1 , . . . , Sn programs on A.
We will call IF ⊆ A × A∗∗ program as Branch of
(π1 : S1 , . . . , πn : Sn ) if ∀a ∈ A:
n
[
IF (a) = wi (a) ∪ w0 (a)
i=1
Si (a) if πi (a),
where ∀i ∈ [1..n] : wi (a) =
∅ else
haaa . . .i if ∀i ∈ [1..n] : ¬πi (a),
w0 (a) =
∅ else
Gergely Feldhoffer Programming methodology
Course Introduction Program, Solution Specification Elementary programs Structures Deduction Recursion Tools
Sequence Branch Loop Program functions of program structures
Branch
Note that a branch can be non-deterministic: if more than one
condition are true in a state each of the routes can happen.
In states where no branch condition is true, the branch must
abort. This is not the usual approach, as C switch without
default performs SKIP instead of ABORT.
Gergely Feldhoffer Programming methodology
Course Introduction Program, Solution Specification Elementary programs Structures Deduction Recursion Tools
Sequence Branch Loop Program functions of program structures
Loop
Def: Loop
Let π be a condition and S0 a program on A. We will call
DO ⊆ A × A∗∗ a Loop if
∀a ∈
/ dπe : DO(a) = {hai}
∀a ∈ dπe : DO(a) =
{α ∈ A∗∗ : ∃α1 , . . . , αn ∈ A∗∗ : (1)
α = red(concat(α1 , . . . , αn )) ∧ α1 ∈ S0 (a)∧ (2)
∧(∀i ∈ [1..n − 1] : αi ∈ A∗ ∧ (3)
∧αi+1 ∈ S0 (τ (αi )) ∧ π(τ (αi )))∧ (4)
∧((αn ∈ A∞ ) ∨ (αn ∈ A∗ ∧ ¬π(τ (αn ))))} (5)
∪ {a ∈ A∞ : ∀i ∈ N : (6)
∃αi ∈ A∗ : α = red(concat(α1 , α2 , . . .))∧ (7)
α1 ∈ S0 (a) ∧ (∀i ∈ N : αi ∈ A∗ ∧ (8)
αi+1 ∈ S0 (τ (αi )) ∧ π(τ (αi )))} (9)
Gergely Feldhoffer Programming methodology
Course Introduction Program, Solution Specification Elementary programs Structures Deduction Recursion Tools
Sequence Branch Loop Program functions of program structures
Loop
So the loop is the repetition of the loop body where the
resulting program string is a concatenation of the iterations
(2) where the iterations are finite in the first n − 1 cases (3),
all of the iterations starts where the previous one ended (4)
and the loop condition is true(4), and the end of this line may
be infinite or such kind of finite where the end of the last
iteration goes outside of the loop conditions truth set(5),
or, the string of the loop can be endless without aborting if
there are infinite number of finite iterations where the loop
condition is always true for the end of the strings of iterations
(6-9).
Gergely Feldhoffer Programming methodology
Course Introduction Program, Solution Specification Elementary programs Structures Deduction Recursion Tools
Sequence Branch Loop Program functions of program structures
Program function of sequence
Composition of relations R1 ⊆ A × B, R2 ⊆ B × C :
R2 ◦ R1 = {(a, c) ∈ A × C : ∃b ∈ B : (a, b) ∈ R1 ∧ (b, c) ∈ R2 }
Strict composition of relations R1 ⊆ A × B, R2 ⊆ B × C :
R2 R1 = {(a, c) ∈ A × C : ∃b ∈ B : (a, b) ∈ R1 ∧ (b, c) ∈
R2 ∧ R1 (a) ⊆ DR2 }
Theorem: Program function of sequence
If S = (S1 ; S2 ) sequence of S1 , S2 programs
p(S) = p(S1 ) p(S2 )
Gergely Feldhoffer Programming methodology
Course Introduction Program, Solution Specification Elementary programs Structures Deduction Recursion Tools
Sequence Branch Loop Program functions of program structures
Program function of branch
Theorem: Program function of branch
∗∗ is a branch, then
n : Sn ) ⊆ A × A
If IF (π1 : S1 , . . . , πW
n
Dp(IF ) = {a ∈ A : i=1 πi (a) ∧ ∀i ∈ [1 . . . n] : πi (a) ⇒ a ∈ Dp(Si ) }
n
[
∀a ∈ Dp(IF ) : p(IF )(a) = pwi (a)
i=1
p(Si )(a) if πi (a),
where ∀i ∈ [1..n] : pwi (a) =
∅ else
So the program function of IF is defined in states where at least
one condition is true, and no Si hangs there, so it will certeanly
terminate, and every possible pathway is included where the
condition is true.
Gergely Feldhoffer Programming methodology
Course Introduction Program, Solution Specification Elementary programs Structures Deduction Recursion Tools
Sequence Branch Loop Program functions of program structures
Program function of loop
Any homogeneous R relation can be composed with itself.
R n = R ◦ R n−1 where R 0 is the identity.
Def: Exclosure of relation
If R ⊆ A × A is a relation, the exclosure of R is R̄ ⊆ A × A where
DR̄ = {a ∈ A : @α ∈ A∞ : α1 ∈ R(A) ∧ ∀i ∈ N : αi+1 ∈ R(αi )}
∀a ∈ DR̄ : R̄(a) = {b ∈ A|∃k ∈ N0 : b ∈ R k (a) ∧ b ∈/ DR }
So the resulting relation contains every (a, b) pair where there is a
path to reach b from a, and there is no step further from b
available.
Gergely Feldhoffer Programming methodology
Course Introduction Program, Solution Specification Elementary programs Structures Deduction Recursion Tools
Sequence Branch Loop Program functions of program structures
Program function of loop
If R ⊆ A × A and B ⊂ A then R|B = {(a, b) ∈ B × A : (a, b) ∈ R}
This is the restriction of the relation to a subset.
Def: Restriction to condition
If R ⊆ A × A and π ⊆ A × L then
R|π = (R ∩ (dπe × A)) ∪ {(a, a) ∈ A × A : a ∈ dπe \ DR }
So the restriction to a condition differs from the restriction to the
truth set of the condition as it is broadened with identities, making
DR|π = dπe
Gergely Feldhoffer Programming methodology
Course Introduction Program, Solution Specification Elementary programs Structures Deduction Recursion Tools
Sequence Branch Loop Program functions of program structures
Program function of loop
Theorem: Program function of loop
If DO(S0 , π) is a loop then
p(DO) = p(S0 )|π
Gergely Feldhoffer Programming methodology
Course Introduction Program, Solution Specification Elementary programs Structures Deduction Recursion Tools
Deduction rules Sequence Branch Loop
Deduction rules
We will give a set of deduction rules for program structures. As
every program can be expressed as a hierarchical structure where
the nodes of the hierarchy are program structures and the leaves
are elementary programs, rules for each structure is enough to
deduce every program.
Gergely Feldhoffer Programming methodology
Course Introduction Program, Solution Specification Elementary programs Structures Deduction Recursion Tools
Deduction rules Sequence Branch Loop
Deduction rules for sequence
Deduction rules for sequence
Let S = (S1 ; S2 ) be a sequence, and Q, R, Q 0 ⊆ A × L statements
on A. If
1 Q ⇒ wp(S1 , Q 0 ) and
2 Q 0 ⇒ wp(S2 , R),
then Q ⇒ wp(S, R).
Gergely Feldhoffer Programming methodology
Course Introduction Program, Solution Specification Elementary programs Structures Deduction Recursion Tools
Deduction rules Sequence Branch Loop
Deduction rules for branch
Deduction rules for branch
Let IF = (π1 : S1 . . . πn : Sn ) be a branch and Q, R ⊆ A × L
statements on A. If
Wn
1 Q ⇒
i=1 πi , and
2 ∀i ∈ [1 . . . n] : Q ∧ πi ⇒ wp(Si , R),
then Q ⇒ wp(IF , R).
Gergely Feldhoffer Programming methodology
Course Introduction Program, Solution Specification Elementary programs Structures Deduction Recursion Tools
Deduction rules Sequence Branch Loop
Deduction rules for loop
Deduction rules for loop
Let DO(π, S0 ) be a loop, P, Q, R ⊆ A × L statements and
t : A → Z function. If
1 Q⇒P
2 P ∧ ¬π ⇒ R
3 P ∧ π ⇒ wp(S0 , P)
4 P ∧π ⇒t >0
5 P ∧ π ∧ t = t0 ⇒ wp(S0 , t < t0 )
then Q ⇒ wp(SO, R)
Gergely Feldhoffer Programming methodology
Course Introduction Program, Solution Specification Elementary programs Structures Deduction Recursion Tools
Deduction rules Sequence Branch Loop
Deduction rules for loop
P is the loop invariant, and t is the terminating function.
P must be true all along the loop and even after the last iteration.
P definitely not equals π, as the second role shows. P is the
connection between the start and the end of the loop iteration
chain.
The hard part of proving the correctness of a program is to guess
P.
t should be used to confirm that the loop is not infinite. The value
of t(a) must be decreased along the loop body borders in each
iteration, and must be positive. As an integer function infinite
regression cannot happen.
Gergely Feldhoffer Programming methodology
Course Introduction Program, Solution Specification Elementary programs Structures Deduction Recursion Tools
Deduction rules Sequence Branch Loop
behold, adventurer
no slides beyond
Gergely Feldhoffer Programming methodology
Course Introduction Program, Solution Specification Elementary programs Structures Deduction Recursion Tools
todo
todo
Gergely Feldhoffer Programming methodology
Course Introduction Program, Solution Specification Elementary programs Structures Deduction Recursion Tools
todo
todo
Gergely Feldhoffer Programming methodology
