Specification and Verification

Specification and Verification I

 

 

Syntax and semantics:

• symbol: V₁ ,..., V_n

  • e.g. X, R, Q etc.

  • denote arbitrary variables

• expressions : E₁, ... , E_n

  • e.g. X + 1

  • denote values

• statements S₁, ... , S_n

  • e.g. X < Y

  • denotes conditions which evaluate to booleans

  • built from

    • booleans

    • relational operators on expressions

    • predicates on expressions

      • e.g. ODD(X), (X+1)² >= X²

  • compound statements built from above using logical operators

    • not, and, or, implies, iff

• commands C₁, ... , C_n

  • denotes, arbitrary commands as follows

 

Commands

• assignment

  • V := E

• array assignment

  • V(E₁) = E₂

• sequences

  • C₁; ... ; C_n

• blocks

  • begin var V₁; ... ; var V_n ; C end

  • semantics:

    • command C is executed

    • variables V₁ ... V_n are returned to their value before the block

• one armed conditional

  • if S then C

• two armed conditional

  • if S then C₁ else C₂

• while

  • while S do C

• for

  • for V := E₁ until E₂ do C

  • semantics

    • if then execute C with value of V increasing each time etc.

    • E₁ and E₂ are evaluated once to get e₁ and e₂

    • if e₁ or e₂ are not numbers or if e₂ < e₁ then nothing is done

    • if e₁ <= e₂ the for command is equivalent to

begin var V; v:=e₁; C ; v:=e₁+1; C ; ... ; v:=e_n; C end

 

 

Hoare notation

• {P} C {Q}

• where

  • P is preconditions

  • C is a program from the language specified above

  • Q is postconditions

• partial correctness specification

  • {P} C {Q}

  • it is not necessary for C to terminate

  • but if C does terminate then Q holds

• total correctness specification

  • [P] C [Q]

  • whenever C is executed in a state satisfying P then C terminates

  • after termination Q holds

• total correctness = partial correctness + termination

 

auxiliary (or ghost) variables

• {X=x /\ Y=y} begin R := X; X := Y; Y := R {X=y, Y=x}

  • x and y are auxiliary variables

 

Floyd-Hoare logic

• |- S means S has a proof

  • statements that have proofs are called theorems

• assignment axiom

  • |- {P[E/V]} V :=E {P}

    • [E/V] is substituting term E for all occurrences of variable V

  • it is not

    • |- {P} V :=E {P[V/E]}

    • |- {P} V :=E {P[E/V]}

  • does not hold when the E can have side effects on the state

• precondition strengthening

|- P => P' |- {P'} C {Q}

---------------------------------

|- {P} C {Q}

•  

  • e.g.

|- X=n => X+1=n+1 |- {X+1=n+1} X := X + 1 {X=n+1}

------------------------------------------------------------------------------

|- {X=n} X := X + 1 {X=n+1}

• postcondition weakening

|- {P} C {Q'} |- Q' => Q

---------------------------------------

|- {P} C {Q}

• specification conjunction

|- {P₁} C {Q₁} |- {P₂} C {Q₂}

-------------------------------------------

|- {P₁ /\ P₂} C {Q₁ /\ Q₂}

• specification disjunction

|- {P₁} C {Q₁} |- {P₂} C {Q₂}

-------------------------------------------

|- {P₁ \/ P₂} C {Q₁ \/ Q₂}

 

• sequencing rule

|- {P} C₁ {Q} |- {Q} C₂{R}

------------------------------------------

|- {P} C₁; C₂ {R}

• the derived sequencing rule

|- P => P₁

|- {P₁} C₁ {Q₁} |- Q₁ => P₂

... ...

|- {P_n} C₁ {Q_n} |- Q_n => Q

----------------------------------------

|- {P} C₁ ; ... ; C_n {Q}

• the block rule

|- {P} C {Q}

--------------------------------------------------

|- {P} begin var V₁; ... var V_n ; C end {Q}

where none of V₁ ... V_n occur in P or Q

• the derived block rule

|- P => P₁

|- {P₁} C₁ {Q₁} |- Q₁ => P₂

... ...

|- {P_n} C₁ {Q_n} |- Q_n => Q

-----------------------------------------------------

|- {P} begin var V₁ ; ... ; V_n ; C₁ ; ... ; C_n {Q}

• the conditional rules

|- {P /\ S} C {Q} |- P /\ ¬S => Q

---------------------------------------------

|- {P} if S then C {Q}

 

|- {P /\ S} C₁ {Q} |- {P /\ ¬S} C₂ {Q}

-------------------------------------------------

|- {P} if S then C₁ else C₂ {Q}

• the case rule

?

• the while rule

|- {P /\ S} C {P}

-----------------------------------

|- {P} while S do C {P /\ ¬ S}

•  

  • e.g.

|- {X=R+(Y*Q)} begin R:=R-Y; Q:=Q+1 end {X=R+(Y*Q)}

|- {X=R+(Y*Q) /\ Y<=R} begin R:=R-Y; Q:=Q+1 end {X=R+(Y*Q)}

by precondition strengthening

|- {X=R+(Y*Q)}

while Y<=R do

begin R:=R-Y; Q:=Q+1 end

{X=R+(Y*Q) /\ ¬(Y<=R)}

by the while rule

|- {T}

while Y<=R do

begin R:=R-Y; Q:=Q+1 end

{X=R+(Y*Q) /\ R<Y)}

by various other rules

 

• the for rule

  • is difficult to define properly

given

|- {P} C {P[V+1/V]}

suppose

C contains no assignments to V

then

|- {V=v} C {V=v}

|- {P /\ (V=v)} {P[V+1/V] /\ (V=v)} by specification conjunction

also consider V:=v; C

|- {P[v/V]} V:=v {P /\ (V=v)}

then

|- {P[v/V]} V:=v; C {P[V+1/V] /\ (V=v)} by the sequencing rule

|- P[V+1/V] /\ (V=v) => P[v+1/V] by logic

hence

|- {P[v/V]} V:=v; C {P[v+1/V]} by postcondition weakening

|- {P[e₁/V]}V:=e₁; C; ... V:= e₂; C {P[e₂/v]}

which suggests a rule

|- {P} C {P[V+1/V]}

-------------------------------------------------------------

|- {P[E₁/V]} for V := E₁ until E₂ do C {P[E₂ + 1/V]}

but it doesn't work, e.g.

since |- {P} X:=Y+1 {P[Y+1/Y]}

|- {X=3} for Y:=3 until 1 do X:=Y+1 {X=2} shouldn't do anything as 3<1

instead try

|- {P} C {P[V+1/V]}

---------------------------------------------------------------------------

|- {P[E₁/V] /\ E₁ <= E₂} for V := E₁ until E₂ do C {P[E₂ + 1/V]}

but

since |- {Y=1} Y:=Y-1 {Y+1=1}

|- {1=1 /\ 1<=1 } for y:=1 until 1 do Y := Y-1 {2=1}

where 1=1 is P[1/Y]

2=1 is P[1+1/Y]

hence end up with

|- {P /\ (E₁ <= V) /\ (V <= E₂)} C {P[V+1/V]}

---------------------------------------------------------------------------

|- {P[E₁/V] /\ E₁ <= E₂} for V := E₁ until E₂ do C {P[E₂ + 1/V]}

where V is not assigned to in C

any variable occurring in E₁ or E₂ is not assigned to

• the for axiom

|- {P /\ (E₂ < E₁)} for V:=E₁ until E₂ do C {P}

• the array assignment axiom

|- {P[A{E₁ <- E₂}/A]} A(E₁):=E₂ {P}

where A{E₁ <- E₂} is an array the same as A except that the value at E₁ is E₂

i.e. treat an array assignment as a normal assignment

• the array assignment axioms

|- A{E₁ <- E₂}(E₁) = E₂

¬(E₁ = E₃) => |- A{E₁<-E₂) = A(E₃ )

 

 

soundness and completeness

• soundness

  • where there is a logical proof then that construct is in the language

  • methods of doing this

    • define the language by the axioms and rules of the logic

      • is axiomatic semantics

      • though it is impossible to construct Floyd Hoare logic for some constructs

    • prove that the logic fits the language

      • prove the axioms and rules of the logic to be valid

      • have a function

        • Meaning(C, s) = s', the resultant state of executing C in state s

        • {P} C {Q} is then true if

          • whenever

            • P is true in state s, and

            • Meaning(c)(s) = s'

          • then

            • Q is true in state s'

• completeness

  • every true specification can be proved

  • how distinguish incompleteness arising due to incompleteness in the assertion language (e.g. arithmetic)

• it is impossible to give a soundness and completeness system for a language combining

  • procedures as parameters of procedure calls

  • recursion

  • static scopes

  • global variables

  • internal procedures as parameters of procedure calls

 

Mechanising program verification

• it is impossible in principle to design a decision procedure to decide automatically the truth or falsehood of an arbitrary mathematical statement

• can mechanise parts of verification

• it is possible to check whether an arbitrary formal proof is valid

• backwards proof:

  • from a statement generate subgoals, prove them and combine them

• to prove {P}C {Q}

  • program C is annotated by inserting into it statements expression conditions that are meant to hold at various intermediate points (automation is AI)

  • a set of verification conditions are generated mechanically

  • verification conditions are proved (automation is AI)

 

Annotation

• annotated command with assertions embedded within it

• a command is properly annotated if statements have been inserted at the following places

  • before each command C_i in a sequence C_i ; ... ; C_n which is not an assignment command

  • after the DO in while and for commands

• a properly annotated specification {P} C {Q} is one where C is a properly annotated command

Verification condition generation

• the justifications assume that the verification conditions have been proved

  • “when C is not an assignment command, then if the result holds for the constituent commands of C (this is called the induction hypothesis), then it holds also for C”

  • most of the justifications can be done using the relevant rule as previously, because the VCs are basically the preconditions to these rules

• assignment command {P} V:= E {Q}

  •  

    • P => Q[E/V]

  • justification

|- {Q[E/V]} V:=E {Q} by the assignment axiom

|- {P} V:= E {Q} by precondition strengthening using P=>Q[E/V]

• one armed conditional {P} if S then C {Q}

  •  

    • (P /\ ¬S) => Q

    • the verification conditions generated by {P /\ S} C {Q}

  • justification

|- (P /\ ¬S) => Q

|- {P /\ S} C {Q} by the induction hypothesis

|- {P} if S then C {Q} by the one armed conditional rule

• two armed conditional {P} if S then C₁ else C₂ {Q}

  •  

    • the verification conditions generated by {P /\ S} C₁ {Q}

    • the verification conditions generated by {P /\ S} C₂ {Q}

  • justification

|- {P /\ S} C₁ {Q} by the induction hypothesis

|- {P /\ S} C₂ {Q} by the induction hypothesis

|- {P} if S then C₁ else C₂ {Q} by the two armed conditional rule

• sequences {P} C₁ ; ... ; C_n-1 ; {R} C_n {Q}, where C_n is not an assignment

  •  

    • the verification conditions generated by {P} C₁ ; ... ; C_n-1 {R}

    • the verification conditions generated by {R} C_n {Q}

  • justification

|- {P} C₁ ; ... ; C_n-1 {R} by induction

|- {R} C_n {Q} by induction

|- {P} C₁ ; ... ; C_n-1 ; C_n {Q} by the sequencing rule

• sequences {P} C₁ ; ... ; C_n-1 ; V:=E {Q}

  •  

    • the verification conditions generated by {P} C₁ ; ... ; C_n-1 {Q[E/V]}

  • justification

|- {P}C₁ ; ... ; C_n-1 ; {Q[E/V]} by induction

|- {Q[E/V}]} V:=E {Q} by the assignment axiom

|- {P}C₁ ; ... ; C_n-1 ; V:=E {Q} by the sequencing rule

• blocks {P} begin var V₁ ; ... ; var V_n ; C end {Q}

  •  

    • the verification conditions generated by {P} C {Q}

    • the syntactic condition that none of V₁ ... V _n are in either P or Q

  • justification

|- {P} C {Q} by induction

|- {P} begin var V₁ ; ... ; var V_n ; C end {Q} by the block rule

• while commands {P} while S do {R} C {Q}

  •  

    • P => R

    • R /\ ¬S => Q

    • the verification conditions generated by {R /\ S} C {R}

  • justification

|- {R /\ S} C {R} by induction

|- {R} while S do C {R /\ ¬S} by the while rule

|- {R} while S do C {Q} by the consequence rules

• for commands {P} for V:= E₁ until E₂ do {R} C {Q}

  •  

    • P => R[E₁/V]

    • R[E₂ + 1/V] => Q

    • P /\ E₂ < E₁ => Q

    • the verification conditions generated by {R /\ E₁ <= V /\ V <= E₂} C {R[V+1/V]}

    • the syntactic condition that C doesn't assign to V or any variable occurring in E₁or E₂

  • justification: long and probably unnecessary

 

Total correctness

• deriving from Floyd Hoare logic

|- {P} C {Q}

---------------

|- [P] C [Q]

if C contains no while commands

• termination of assignments

  • assumes all function calls/applications in the expression on the RHS terminate

    • that might not be true if

      • the functions are defined recursively

      • erroneous expressions like 1/0 cause problems

  • [T] X := 1/0 [X = 1/0] is valid, hence

    • 1/0 is some number

    • 1/0 is some error value

  • if have error values have messy laws of arithmetic

  • assume that arithmetic expressions always denote numbers

    • in some cases exactly what number is not specified

¬(n=0) => (m/n)*n = m

• while rule for total correctness

  • can use if can prove some non-negative quantity (the variant) decreases with each iteration

|- [P /\ S /\ (E=n)] C [P /\ (E<n)] |- P /\ S => 0 <= E

---------------------------------------------------------------------------

|-[P] while S do C [P /\ ¬S]

where

E is the variant (an integer valued expression)

n is an auxiliary variable not occurring in P, C, S or E use to ensure the variant is decreasing

•  

  • e.g. |- [Y>0] while Y<=R do begin R:=R-Y; Q:=Q+1 end [T]

where

P = Y > 0

S = Y <= R

E = R

C = begin R:=R-Y; Q:=Q+1 end

• termination specification

  • formalisation of total correctness = partial correctness + termination

|- {P} C {Q} |- [P] C [T]

----------------------------------------

|- [P] C [Q]

 

|- [P] C [Q]

----------------------------------------

|- {P} C {Q} |- [P] C [T]

 

Verifications conditions for total correctness

• while commands

  • need to add a variant as an annotation

  • [P] while S do {R}[E] C [Q]

    • R is the invariant: needs to be true each time control reaches it

    • E is the variant

  • conditions

    • P => R

    • R /\ ¬S => Q

    • R /\ S => E >= 0

    • the verification conditions generated by [R /\ S /\ (E=n)] C [R /\ (E<n)]

    • the condition that n is a ghost variable not occurring in P, C, S, R, E or Q

• other commands

  • exactly the same as partial correctness but with square brackets instead of curly ones

 

Program refinement

• specifications

  • programming constructs

  • same role as commands

  • not directly executable

  • guaranteed to achieve a given postcondition from a given precondition

  • specification is identified with its set of possible implementations

    • [P, Q] = { C |- [P] C [Q] }

• refinement represented as manipulations on sets of ordinary commands

• a refinement has the form

  • 

  • each intermediate state is obtained from its predecessor by application of a refinement law

• wide spectrum language: generalised programming language containing

  • pure specifications

  • pure code

  • mixtures of the two

• refinement laws

  • general method of generation for [P, Q] ⊇ ζ C₀ ... C_n

    • where

      • words in blue are sets of programs

      • words in green are programs

      • ζ is the generalisation of a construct using programs or sets of programs

        • one such construct is while S do C (which is a program itself)

        • another is if then [P/\S, Q] else [P/\¬S, Q] (which is a set of programs itself)

1.  
   1.  

      1. define ζ C₀ ... C_n = {ζ C₀ ... C_n| C₀ C₀ ... C_n C_n}

         1. e.g. if S then [P /\ S, Q] else [P /\ ¬S, Q] = {if S then C₀ else C₁ | C₀ [P /\ S, Q] /\ C₁ [P /\ ¬S, Q]}

         2. C₀ is equivalent to [P₀, Q₀], for appropriate P₀ and Q₀

      2. assume C ζ C₀ ... C_n

         1. where C is a ζ C₀ ... C_n

      3. deduce C {ζ C₀ ... C_n| C₀ [P₀, Q₀] ... C_n [P_n, Q_n]} (by 1.ii)

      4. deduce C {ζ C₀ ... C_n| |- [P₀] C₀ [Q₀] ... |- [P_n] C_n [Q_n] }

         1. as C_i [P_i, Q_i] <=> |- [P_i] C_i [Q_i]

      5. use a Hoare Logic rule to combine the [P_i] C_i [Q_i] to get

C {ζ C₀ ... C_n| |- [P] ζ C₀ ... C_n [Q] }

1.  
   1.  

      1. deduce C [P, Q]

         1. by definition of [P, Q]

•  
  •  

    • logically

C ζ C₀ ... C_n = {ζ C₀ ... C_n| C₀ C₀ ... C_n C_n}

<=> C {ζ C₀ ... C_n| C₀ [P₀, Q₀] ... C_n [P_n, Q_n]}

<=> C {ζ C₀ ... C_n| |- [P₀] C₀ [Q₀] ... |- [P_n] C_n [Q_n] }

=> C {ζ C₀ ... C_n| |- [P] ζ C₀ ... C_n [Q] }

(one way as Hoare rules are not iff)

<=> C [P, Q]

•  

  • our wide spectrum language

C₀ ; ... ; C_n = {C₀ ; ... ; C_n| C₀ C₀ /\ ... /\ C_n C_n}

begin var V₁ ; ... V_n ; C end = {begin var V₁ ; ... V_n ; C end | CC }

if S then C = {if S then C | CC}

if S then C₁ else C₂ = {if S then C₁ else C₂ | C₁C₁ /\ C₂C₂}

while S do C = {while S do C | CC}

•  
  •  

    • NB these wide spectrum commands are monotonic, i.e.

      • if C₀ ⊇ C'₀ /\ ... /\ C_n ⊇ C'_n then C₀ ; ... ; C_n ⊇ C'₀ ; ... ; C'_n

  • laws

    • skip law: [P, P] ⊇ {skip}

    • assignment law: [P[E/V]] ⊇ {V:=E}

    • derived assignment law: [P, Q] ⊇ {V:=E}

      • if |- P => Q[E/V]

    • precondition weakening: [P, Q] ⊇ [R, Q]

      • if |- P => R

    • postcondition strengthening: [P, Q] ⊇ [P, R]

      • if |- R => Q

    • sequencing law: [P, Q] ⊇ [P, R] ; [R, Q]

    • block law: [P, Q] ⊇ begin var V; [P, Q] end

      • where V does not occur in P or Q

    • one armed conditional law: [P, Q] ⊇ if S then [P /\ S, Q]

      • if |- P /\ ¬S => Q

    • two armed conditional law: [P, Q] ⊇ if S then [P /\ S, Q] else [P /\ ¬S, Q]

    • while law: [P, P /\ ¬S] ⊇ while S do [P /\ S /\ (E=n), P /\ (E<n)]

      • if |- P /\ S => E >= 0

 

First order logic

• notation

  • predicates P(x)

  • ¬t

  • t₁ /\ t₂

  • t₁ \/ t₂

  • t₁ => t₂

  • t₁ /\ t₂

  • ∀x . t[x]

  • ∃x . t[x]

  • ∃!x . t[x] (unique x s.t. t[x])

• statements and formulae regarded as boolean valued (i.e. cannot return a function, etc.)

  • t[x] is just a boolean term containing variable x

 

 

Higher order logic (HOL)

• terms (notation)

  • variables

    • range over functions and predicates

    • e.g. x, y, P

  • constants

    • stand for fixed values

    • e.g. T, F, 0, 1, ... , +, *, <, <=, ∀, ∃

  • function applications

    • t₁ t₂

    • binary function constants can be infixed (i.e. write t₁ + t₂ instead of + t₁ t₂)

  • abstractions (lambda terms)

    • denote functions

    • λx . t

      • where x is a variable

• allows higher order variables

  • e.g. ∀P . [ P(0) /\ (∀n . P(n) => P(n+1)) => ∀n . P(n) ] for induction on natural numbers

• types

  • NB Russell's paradox: P x = ¬(x x) => P P = ¬(P P)

  • types are expressions which denote sets of values

  • atomic types

    • bool

    • ind – individuals

    • num – natural numbers

    • real

  • compound types: built from other types

    • if σ, σ₁ and σ₂ are types then the following are types

      • σ list

      • σ₁ -> σ₂

      • σ₁ x σ₂

  • terms of HOL must be well typed

    • it must be possible to assign a type to each subterm s.t. The following hold

1.  
   1.  

      1. for every application subterm t₁ t₂ there are types σ₁, σ₂ s.t.

•  
  •  

    • t₁ is σ₁ -> σ₂

    • t₂ is σ₁

    • t₁ t₂ is σ₂

1.  
   1.  

      1. for every lambda subterm λx . t there are types σ₁, σ₂ s.t.

•  
  •  

    • x is σ₁

    • t is σ₂

    • λx.t is σ₁ -> σ₂

•  

  • variables of the same name can be assigned different types, e.g. x:σ₁ , x:σ₂

    • if they are then they are considered to be separate variables

  • polymorphic types

    • type variable

      • can instantiate the type variable with any type

      • e.g. twice = λf. λx. f(f(x)): (α -> α) -> α -> α

    • a type which contains a type variable is a polymorphic type

      • otherwise called monomorphic

• binders: used to syntactic sugar

  • write f x.t instead of f ( λx.t)

  • with quantifiers

•  
  •  

    • ∀ ∃ are constants

    • ∀x.t considered 'user friendly syntax' for ∀ (λx.t), i.e. a function applied to ∀

    • ∀ : (α -> bool) -> bool

• pairs and tuples

  • (t₁, t₂) : σ₁ x σ₂ if t₁:σ₁ /\ t₂:σ₂

  • (t₁, t₂, ... , t_n) is an abbreviation for ((...(t₁, t₂) , ... ), t_n)

• lists

  • type σ list

  • nil: σ list

  • cons: σ -> σ list -> σ list

• conditionals

  • cond t t₁ t₂ = (t -> t₁ | t₂) = “if t then t₁ else t₂)

• Hilbert's ε operator

  • ε x. t[x]

where

x: σ

t[x]:bool (is a boolean term containing free variable x)

•  
  •  

    • denotes some value of type σ which satisfies t[a] (makes it true)

    • if there is no x:σ which satisfies t[x] then it denotes some fixed unspecified value of type σ

  • e.g. ε x. x=2 would be 2

  • e.g. ε x. x<2 would be some unspecified number which is less than 2

  • can define several other things usually taken to be primitive using ε-operator

    • conditionals

      • cond t t₁ t₂ = ε x. ((t = T) => (x = t₁)) /\ ((t = F) => (x = t₂))

= ε x. (¬(t = T) \/ (x = t₁)) /\ (¬(t = F) \/ (x = t₂))

•  
  •  

    • lambda abstraction

      • λx.t = ε f.∀x. f(x) = t

assuming variable f does not occur in the term t

•  
  •  
    •  

      • “the function f such that f(x) = t for all x”

      • e.g. fact n = ε f.∀n. (f(0) = 1) /\ (f(n+1) = (n+1)*f(n))

• Axiom of choice

  • set theory

  • if S is a set of non-empty sets, for each non empty XS then there exists a function Choose s.t. choose(X)X

  • inclusion of Hilbert's ε operator automatically builds this in

  • details

    • sets are not primitive in HOL

    • instead use characteristic functions such as f_X

      • maps from items to {T, F}

      • f_X(x) = T iff xX

    • have to work on characteristic functions rather than directly on sets

    • in HOL

      • assert there is a function Select s.t. P(Select(P)) = T

        • assuming P is the characteristic function of a non-empty set

      • hence Select P = Choose {x | P x = T}

        • they aren't the same as Choose works on sets and Select on characteristic functions

  • ε is a binder for Select s.t. ε: (σ -> bool) -> σ, so if P:(σ -> bool)

    • ε(P) denotes some fixed (but unknown) value x s.t. P(x) = T

    • if no such value exists (i.e.∀x . P(x) = F)then ε(P) denotes some unspecified value in the set, denoted by σ

 

• definitions

  • definitions are axioms of the form

    |- c = t

where c is a new constant

t is a closed term that doesn't contain c

•  

  • function definitions

    |- f = λ x₁ ... x_n . t

    can be written as

    |- f x₁ ... x_n = t

  • adding a new definition to the set of existing ones cannot introduce any new inconsistencies

• natural numbers

  • introduce

    • a type num

    • constant 0 : num

    • Suc : num -> num

  • postulate Peano's Axioms

1.  

   1. there is a number 0

   2. there is a function Suc called the successor function s.t. if n is a number then Suc n is a number

   3. 0 is not the successor of any other number

•  
  •  

    axiomatic formalisation: |- ∀m . ¬(Suc m = 0)

1.  

   1. if two numbers have the same successor then they are equal

•  

  axiomatic formalisation: |- ∀m n . (Suc m = Suc n) => (m = n)

1.  

   1. if a property holds of 0 and if whenever it holds of a number then it also holds of the successor of the number then the property holds of all numbers (mathematical induction)

•  

  axiomatic formalisation:

|- ∀P: num -> bool . [P 0 /\ (∀m . P m => P(Suc m))] => ∀m. P m

• primitive recursion

•  

  • basic primitive recursive functions are given by these axioms:

1. Constant function: The 0-ary constant function 0 is primitive recursive.

2. Successor function: The 1-ary successor function Suc is primitive recursive.

3. Projection function: ∀n i . n≥1 /\ 1≤i≤n the n-ary projection function P_iⁿ, which returns its i-th argument, is primitive recursive.

•  

  • complex primitive recursive functions are obtained by applying the operators given by the axioms:

1. Composition:

•  

  • given

    • f, a k-ary primitive recursive function

    • k m-ary primitive recursive functions g₁,...,g_k

  • the composition of f with g₁,...,g_k,

    h(x₁,...,x_m) = f(g₁(x₁,...,x_m),...,g_k(x₁,...,x_m))

    is primitive recursive

1. Primitive recursion:

•  

  • given

    • f, a k-ary primitive recursive function

    • g, a (k+2)-ary primitive recursive function

  • the (k+1)-ary function defined as the primitive recursion of f and g

    h(0,x₁,...,x_k) = f(x₁,...,x_k)

    h(S(n),x₁,...,x_k) = g(h(n,x₁,...,x_k),n,x₁,...,x_k)

    is primitive recursive.

 

•  

  • to enable recursive 'definitions' (e.g. |- 0 + m = m) use Primitive Recursive Theorem

    |- ∀x:α . ∀f :α -> num -> α . ∃fun: num->α . (fun 0 = x) /\ (∀m . fun(Suc m) = f (fun m ) m

  • e.g. for +

    • specialise x to be λn.n

    • specialise f to be λf' x' . λn . Suc(f' n)

    • this yields

|- ∃fun . (fun 0 = x) /\ [m . fun(Suc m) = λf' x' . λn . Suc (f' n) (fun m) m]

<=> |- ∃fun . (fun 0 = x) /\ [fun (Suc m) n = Suc(fun m n)]

 

FINISH THIS LATER – probably not the most important thing in the world

 

• semantics

  • types denote sets

  • terms denote members of these sets

  • if t:σ then we can consider t to denote a member of the set denote by σ

  • type schemes

    • a type scheme σ includes type variables α₁, ... α_n

    • is not a set (a type) but a class function

    • it is a function from m tuples of sets to sets

      • e.g. if γ_i represents an arbitrary set (with no type variables) a type scheme represents the relation

        γ₁ x γ₂ x ... x γ_n x γ'

    • e.g. α → α is the class function (relation) such that

      γ |→ {f | f : γ → γ}

      • maps type γ to the set of functions of type γ → γ

  • polymorphic constants

    • these are interpreted as the functions of the interpretations of the type variables in their type

    • e.g. Id: α→α is the function from a type to the identity function on that type

 

Semantic embedding

wff ::= True | N wff | C wff wff | D wff wff

• deep embedding

  • represent wff inside the host logic by values of some type (e.g. twff)

  • define a semantic function in the host logic

    •  

      NB, M : twff

    M(True) = T

    M(N w) = ¬M(w)

    M(C w₁ w₂) = M(w₁) /\ M(w₂)

    M(D w₁ w₂) = M(w₁) \/ M(w₂)

  • theorems about the embedded language can be proved, e.g.

    ∀w₁, w₂wff . M(C w₁ w₂) = M(N (D (N w₁) (N w₂)))

• shallow embedding

  • set up notational conventions for translating wff's into terms in the host logic

    • the translation is not defined in terms of the host logic

  • is “parsing and pretty printing”

    [[True]] ~~> “T”

    [[N w]] ~~> “¬” concat [[w]]

    [[C w₁ w₂]] ~~> [[w₁]] concat “/\” concat [[w₂]]

    [[D w₁ w₂]] ~~> [[w₁]] concat “\/” concat [[w₂]]

  • quantification over wff's is not possible

    • hence only theorems in the embedded language can be be proved

• we want to do this for Floyd Hoare logic because then we can derive the logic rules and guarantee their soundness

A shallow embedding of Hoare specifications

E ::= N | V | E₁ + E₂ | E₁ – E₂ | E₁ x E₂ | ...

B ::= E₁ = E₂ | E₁ <= E₂

C ::= skip

| V := E

| C₁ ; C₂

| if B then C₁ else C₂

| while B do C

where

V ranges over program variables

etc.

• axioms

  |- {P} skip {P} (skip)

  |- {P[E/V]} V := E {P} (assignment)

• rules

|- P => P' |- {P'} C {Q}

--------------------------------- (precondition strengthening)

|- {P} C {Q}

 

|- {P} C {Q'} |- Q' => Q

--------------------------------------- (postcondition weakening)

|- {P} C {Q}

 

•  

  • NB, the above have theorems in Hoare logic and in pure logic

    • Hoare logic proofs may require pure logic sub-proofs

|- {P} C₁ {Q} |- {Q} C₂{R}

------------------------------------------ (sequencing)

|- {P} C₁; C₂ {R}

 

|- {P /\ B} C₁ {Q} |- {P /\ ¬B} C₂ {Q}

------------------------------------------------- (if)

|- {P} if B then C₁ else C₂ {Q}

 

|- {P /\ B} C {P}

----------------------------------- (while)

|- {P} while B do C {P /\ ¬ B}

 

•  

  • NB, the above assumes that B is a boolean expression in the language and a formula of the predicate logic

• semantics

  • define Meaning : Commands x States x States

    • this is a partial function, as some things don't terminate, e.g.

      Meaning(while T do C)(s) is undefined

  • we really do need total functions to do predicate calculus, so instead define c to denote (provide the meaning for) a given C_i as:

c(s₁, s₂) = { T if Meaning(C_i)(S₁) = s₂

{F otherwise

• states

  • define the type state = string → num

  • e.g. s = λx . (x = 'X' → 1 | (x = 'Y' → 2 | (x = 'Z' → 3)))

• other denotations: the meanings for E, B and C are provided as

  • e : state → num (this is expressions)

  • b : state → num (this is booleans)

  • c : state x state → bool (this is the c defined previously)

• in the abstract define [[ ... ]] as

  [[ T[X₁, ... , X_n] ]] = λs . [[ T[s 'X₁', ... , s 'X_n'] ]]

  where T[X₁, ... , X_n] is a higher order logic term

  T:σ

  [[T]]: state → σ

• we can define the translation [[ ... ]]

  •  

    where Skip(s₁, s₂) = (s₁ = s₂)

    •  
      •  
        •  
          •  
            •  
              •  
                •  

                  (e s) means evaluating expression e in environment s

                  v is representing something like 'A' so this λx is creating a state

                remember the conventions from earlier

    where Assign(v, e)(s₁, s₂) = (s₂ = Bnd(e, v, s₁))

    Bnd(e, v, s) = λx . (x = v → (e s) | s x)

    where Seq(c₁, c₂)(s₁, s₂) =

    where if(b, c₁, c₂)(s₁, s₂) = b s₁ → c₁(s₁, s₂) | c₂(s₁, s₂)

  [[skip]] ~~> Skip

  [[V := E]] ~~> Assign('V', [[ E ]] )

  [[C₁ ; C₂]] ~~> Seq( [[C₁]], [[C₂]] )

  [[if B then C₁ else C₂]] ~~> If([[B]],[[C₁]],[[C₂]])

  [[while B do C]] ~~> While([[B]], [[C]])

  where while(b, c)(s₁, s₂) =

  Iter(0)(b, c)(s₁, s₂) = F

  Iter(n+1)(b, c)(s₁, s₂) = If(b, Seq(c, Iter(n)(b, c)), Skip)(s₁, s₂)

 

•  

  [[ X ]] ~~> λs . s 'X' i.e. apply 'X' to the state, and get a number back

  [[ E₁ + E₂ ]] ~~> [[ E₁ ]] + [[ E₂ ]]

  etc.

  • NB, that sometimes logical variables must be included in pre and post conditions along with program variables

    •  

      e.g. {X = x, Y = y}

    • define [[ ... ]] such that

      [[X = x /\ Y = y]] ~~> λs . (s 'X') = x /\ (s 'Y') = y

• semantics of partial correctness specifications

  • a partial correctness specification {P} C {Q} denotes

    . [[P]] s₁ /\ [[C]](s₁, s₂) => [[Q]] s₂

  • Spec(p, c, q) = . [[P]] s₁ /\ [[C]](s₁, s₂) => [[Q]] s₂

  • e.g.

    {X = 1} X := X + 1 {X = 2}

    denotes

    Spec(λs . S 'X' = 1, Assign('X', λs . s 'X' + 1), λs . s 'X' = 2)

 

• Floyd-Hoare logic as higher order logic

  • theorems

    |- ∀p . Spec(p, Skip, p)

    |- ∀p v e. Spec((λs.p(Bnd(e, v, s))), Assign(v, e), p)

    |- ∀p p' q c . ((∀s. p' s => p s) /\ Spec(p, c, q)) => Spec(p, c, q')

    |- ∀p q q' c. (Spec(p, c, q) /\ (∀s. q s => s' s)) => Spec(p, c, q')

    |- ∀p q r c₁ c₂ . Spec((λs . P s /\ b s), c₁, q) /\ Spec((λs. P s /\ ¬(b s)), c₂, q)

    => Spec(p, If(b, c₁, c₂), q)

    |- ∀p c b . Spec((λs . P s /\ b s), c, p) => Spec(p, while((b, c), (λs. P s /\ ¬(b s)))

  • the theorems can be derived from the previous definitions of Skip etc.

  • the axioms and rules for Floyd-Hoare logic can then be derived

• termination and total correctness

  • since here Hoare logic is presented as a derived logic it's easy to add extensions and modifications without fear of introducing unsoundness

  • e.g. termination assertion

    Halts(p, c) = ∀s₁ . P s₁ =>s₂ . c(s₁, s₂)

    • note that this means some computation of C starting from state satisfying P will terminate

  • if commands are deterministic

    Det(c) = ∀s s₁ s₂ . c(s, s₁) /\ c(s, s₂ ) => s₁ = s₂

    then termination is adequately formalised by halts, hence

    Total_spec(p, c, q) = Halts(p, c) /\ Spec(p, c, q)

  • theorems can be proven

    •  

      • i.e. if there is a variant x which decreases each time then the loop will terminate

    |- ∀p. Halts(p, skip)

    |- ∀p v e . Halts(p, Assign(v, e))

    |- ∀p p' c . (∀s . p' s => p s) /\ Halts(p, c) => Halts(p', c)

    |- ∀p c₁ c₂ q . Halts(p, c₁) /\ Spec(p, c₁, q) /\ Halts(q, c₂) => Halts(p, Seq(c₁, c₂))

    |- ∀p c₁ c₂ b . Halts(p, c₁) /\ Halts (p, c₂) => Halts(p, If(b, c₁, c₂))

    |- ∀b c x . (∀n . Spec (λs . p s /\ b s /\ s x = n, c, λs . p s /\ s x < n))

    /\ Halts (λs . p s /\ b s, c) => Halts(p, While(b, c))

 

Other programming logic constructs

• Vienna development method

  • is a variation on Hoare style specifications

  • reduces the need for auxiliary logical variables

  • e.g.

    {X = x /\ Y = y} R := X; X := Y; Y := R {X = y /\ Y = x}

    is written as

    {T} R := X; X := Y; Y := R {X = /\ Y = } (actually like /_ rather than _ )

  • option for defining semantics one

    • more generally

      {P[X₁ , ... , X_n]} C {Q[X₁ , ... , X_n,,]}

      can be thought as an abbreviation for

      {P[X₁ , ... , X_n] /\ X₁ =... /\ X_n =} C {Q[X₁ , ... , X_n,,]}

    • this has problems with deducing sequences, e.g.

      {T} X := X + 1 ; X := X + 1 {X = + 2}

      being derived from

      {T} X := X + 1 {X = + 1}

 

•  

  • option for defining semantics two

    • regard

      {P[X₁ , ... , X_n]} C {Q[X₁ , ... , X_n,,]}

      as

      VDM_Spec ([[ P[X₁ , ... , X_n] ]], [[C]], [[ Q[X₁ , ... , X_n,,] ]]₂)

      where

      [[ Q[X₁ , ... , X_n,,] ]]₂ = λ(s₁, s₂) . Q[s₂ 'X₁' , ... , s₂ 'X_n', s₁ 'X₁', ... , s₁ 'X_n']

  • Aczel's version of the while rule

|- {P /\ B} X {P /\ R}

---------------------------------------

|- while B do C {P /\ ¬b /\ R*}

•  
  •  

    where R* is the reflexive closure of R

    R*(s₁, s₂) =

    R⁰ = λ(s₁, s₂) . s₁ = s₂

    Rⁿ⁺¹ = Seq(R, Rⁿ)

    • this version of the while rule can be converted into a rule of total correctness by requiring R to be

      • transitive

        • transitive r =

      • well founded

        Well founded r = ¬: num→state .∀n . r(f(n), f(n+1))

• Dijkstra's weakest preconditions

  • this is used for rigorous program construction

    • not really for post hoc verification

  • weakest predicates

    • given p and q as predicates on states (have type state→bool)

    • p is weaker (less constraining) than q if

      ∀s . q s => p s

    • is written p <= q

    • weakest P = εp . P p /\ ∀p' . P p' => (p <= p')

 

•  

  • weakest liberal preconditions

    • wlp(C, Q) = the weakest predicate P such that {P} C {Q}

    • wlp(c, q) = weakest (λp . Spec(p, c, q))

    • however it is easier to work with the following (which can be shown from the above)

      |- wlp(c, q) = λs. (∀s' . c(s, s') => q s')

 

how do you show it? I don't understand why they're

the same, i.e. I don't see the “weakest” requirement in the second

•  

  • weakest preconditions

    • wp(C, Q) = the weakest predicate P such that [P] C [Q]

    • wp(c, q) = weakest (λp . Total_Spec(p, c, q))

    • however it is easier to work with the following (which can be shown from the above)

      |- wp(c, q) = λs. ((s' . c(s, s')) /\ ∀s' . c(s, s') => q s')

 

•  

  • relation to Hoare notation

    |- Spec(p, c, q) = ∀s . ( s => wlp(c,q) s)

    |- Total_Spec(p, c, q) = ∀s . ( s => wp(c,q) s)

  • if we redefine /\, \/, =>, ¬, T, F and |= so that they can operate on predicates, i.e.

    p /\ q = λs . p s /\ q s

    p \/ q = λs . p s \/ q s

    p => q = λs . p s => q s

    ¬p = λs . ¬p s

    T = λs . T

    F = λs . F

    |= p = ∀s . p s NB. See this used below

  • we can then (re)write the following theorems

    |- Spec(p,c,q) = ∀s . (p => wlp(c, q)) s

    = |= p => wlp(c, q)

    |- Total_Spec(p,c,q) = ∀s . (p => wp(c, q)) s

    = |= p => wp(c, q)

    |- ∀c . |= wp(c, f) = F

    |- ∀q r c . |= (q => r) => (wp(c, q) => wp(c, r))

    |- ∀q r c . |= (wp(c, q) /\ wp(c, r) = wp(c, q /\ r)

    |- ∀q r c . |= (wp(c, q) \/ wp(c, r) => wp(c, q \/ r))

    |- ∀q r c . Det c => (|= (wp(c, q) \/ wp(c, r) = wp(c, q \/ r)))

 

•  
  •  

    |- ∀c . |= wlp(c, f) = λs. ¬s'.c(s, s')

    |- ∀q r c . |= (q => r) => (wlp(c, q) => wlp(c, r))

    |- ∀q r c . |= (wlp(c, q) /\ wlp(c, r) = wlp(c, q /\ r)

    |- ∀q r c . |= (wlp(c, q) \/ wlp(c, r) => wlp(c, q \/ r))

    |- ∀q r c . Det c => (|= (wlp(c, q) \/ wlp(c, r) = wlp(c, q \/ r)))

  • inadequacy: sequences

    • attempting to derive Dijkstra's wp law for sequences

    • ...

 

• Dynamic logic

  • this is a programming logic which emphasizes an analogy between Hoare logic and modal logic

  • in dynamic logic states of computation are thought of as possible worlds

    • if a command C transforms an initial state s to a final state s' then s' is considered accessible from s

  • traditional modal logic would have [] and <> with the interpretations

    []q is true (valid) in s if q is true in all states accessible from s

    <>q is true (valid) in s if ¬[]¬q is true in s

  • however in dynamic logic we have [C] and <C> for each command C

    •  

      where ¬ is negation defined on predicates, as above

    [c]q = λs. (∀s' . c(s, s') => q s')

    <c>q = ¬([c] (¬q))

  • example theorems in modal logic are

    |- ∀c q . Det c => (|= <c>q => [c]q)

    |- (|= [c] q) = Spec(T, c, q)

    |- Det c => (|= <c>q) = Total_Spec(T, c, q)

    |- Spec(p, c, q) = (|= p => [c]q)

    |- Det c => (Total_Spec(p, c, q) = (|= [ => <c> q))

 

•  
  •  

    |- wlp(c, q) = [c] q

    • |- Det c => (wp(c, q) = <c> q)