Scribd
Upload
32 views1 page

Verification Rules

Uploaded by

Alina Erkulova
Copyright
© © All Rights Reserved
We take content rights seriously. If you suspect this is your content, claim it here.
Available Formats
Download as PDF, TXT or read online on Scribd
32 views1 page

Verification Rules

Uploaded by

Alina Erkulova
Copyright
© © All Rights Reserved
We take content rights seriously. If you suspect this is your content, claim it here.
Available Formats
Download as PDF, TXT or read online on Scribd

Program constructs and their verification rules

Sequence
S = (S1 ; S2 ) is the sequence of two programs S1 , S2 . Q, R and Q0 are logical functions over A. If
1. Q =⇒ wp(S1 , Q0 ) and
2. Q0 =⇒ wp(S2 , R)
then Q =⇒ wp(S, R)

S
S1
S2

Selection
IF = (π1 : S1 , . . . , πn : Sn ) is a branches constructed from programs S1 , . . . , Sn and logical functions
π1 , . . . , πn . Q and R are logical functions over A. If
n
W
1. Q =⇒ πi and
i=1
n
V
2. Q =⇒ (πi ∨ ¬πi ) and
i=1

3. ∀i ∈ [1..n] : Q ∧ πi =⇒ wp(Si , R)
then Q =⇒ wp(IF, R)

IF
A π1 · · · A πn
A A
S1 ··· Sn

Loop
DO = (π, S0 ) denotes the loop constructed from the program S0 and the logical function π.
Inv, Q, R are logical functions over A and t : A → Z is a function. If
1. Q =⇒ Inv and
2. Inv ∧ ¬π =⇒ R and
3. Inv =⇒ π ∨ ¬π and
4. Inv ∧ π =⇒ t > 0 and
5. Inv ∧ π ∧ t = t0 =⇒ wp(S0 , Inv ∧ t < t0 ) for any t0 integer number
then Q =⇒ wp(DO, R)
(Inv is called loop invariant, t is called variant function.)

DO
π
S0

You might also like