Z3
Weakest Precondition
LTL
Z3 Questions, Weakest Precondition
Fixed-Points, LTL
Lev Naiman
Department of Computer Science
University of Toronto
CSC410 Tutorial, 10 Feb 2013
Lev Naiman
CSC410
1/20
Z3
Weakest Precondition
LTL
Outline
1
Z3
Questions
2
Weakest Precondition
Weakest Precondition and Fixed-Points
3
LTL
Definition
Semantics
Proving
Lev Naiman
CSC410
2/20
Z3
Weakest Precondition
LTL
Questions
Outline
1
Z3
Questions
2
Weakest Precondition
Weakest Precondition and Fixed-Points
3
LTL
Definition
Semantics
Proving
Lev Naiman
CSC410
3/20
Z3
Weakest Precondition
LTL
Questions
Z3
Note: No credit for code that does not use Z3
The whole point is learning to write formal specifications
For A2Q2 (teaparty question) all the constraint about
maximal distance says is that if a guests starting position is
i and final position j then abs(i − j) ≤ S
Lev Naiman
CSC410
4/20
Z3
Weakest Precondition
LTL
Weakest Precondition and Fixed-Points
Outline
1
Z3
Questions
2
Weakest Precondition
Weakest Precondition and Fixed-Points
3
LTL
Definition
Semantics
Proving
Lev Naiman
CSC410
5/20
Z3
Weakest Precondition
LTL
Weakest Precondition and Fixed-Points
Weakest Precondition
Fixed-Points
Consider the following program S:
while x 6= 0 do
x:=x-1
end
We would like to find wp(S, x = 0). We can either find an
invariant or find a fixed point.
For a fixed-point of a loop while B do Q end and
post-condition P we construct function H as:
H0 (P) = ¬B ∨ P
Hk (P) = wp(if B then Q, Hk −1 (P)) ∨ Hk −1 (P)
Lev Naiman
CSC410
6/20
Z3
Weakest Precondition
LTL
Weakest Precondition and Fixed-Points
Weakest Precondition
Fixed-Points
We need a number n such that Hn = Hn−1 .
This is effectively unrolling the loop until we find a
fixed-point.
We have P = (x = 0) and our body of the loop
Q = (x := x − 1). We proceed as follows:
H0 (x = 0) = ¬(x 6= 0) ∨ (x = 0)
= (x = 0)
Lev Naiman
CSC410
7/20
Z3
Weakest Precondition
LTL
Weakest Precondition and Fixed-Points
Weakest Precondition
Fixed-Points
H1 (x = 0) = wp(if x 6= 0 then x := x − 1, H0 (x = 0)) ∨ H0 (x = 0)
= wp(if x 6= 0 then x := x − 1, x = 0) ∨ x = 0
= (x 6= 0 ⇒ wp(x := x − 1, x = 0)∧
x = 0 ⇒ wp(skip, x = 0)) ∨ x = 0
= (x 6= 0 ⇒ x − 1 = 0) ∧ x = 0 ⇒ x = 0) ∨ x = 0
= x 6= 0 ⇒ x − 1 = 0 ∨ x = 0
=x −1=0∨x =0
=x =1∨x =0
=0≤x ≤1
Lev Naiman
CSC410
8/20
Z3
Weakest Precondition
LTL
Weakest Precondition and Fixed-Points
Weakest Precondition
Fixed-Points
H2 (x = 0) = wp(if x 6= 0 then x := x + 1, H1 (x = 0)) ∨ H1 (x = 0)
=0≤x ≤2
..
.
Hn (x = 0) = 0 ≤ x ≤ n
For what n does Hn = Hn−1 ?
No natural n, but works for ∞
H∞ (x = 0) = 0 ≤ x ≤ ∞
=0≤x
Lev Naiman
CSC410
9/20
Z3
Weakest Precondition
LTL
Weakest Precondition and Fixed-Points
Weakest Precondition
Fixed-Points
Therefore we have proven that
0 ≤ x ⇒ wp(while x 6= 0 do x := x − 1 end, x = 0)
More strongly, in this case x ≥ 0 is the weakest
precondition itself
Note that sometimes proving an expression of the form
P ⇒ wp(S, Q) does not necessarily require finding the
weakest precondition, only showing that P implies it. This
is a similar concept to existential proofs in mathematics.
Lev Naiman
CSC410
10/20
Z3
Weakest Precondition
LTL
Definition
Semantics
Proving
Outline
1
Z3
Questions
2
Weakest Precondition
Weakest Precondition and Fixed-Points
3
LTL
Definition
Semantics
Proving
Lev Naiman
CSC410
11/20
Z3
Weakest Precondition
LTL
Definition
Semantics
Proving
LTL
Definition
Linear Temporal Logic (LTL) references a path of states
denoted π.
References a finite number of states from a state machine
Denote atomic propositions using English letters. A state is
a set of atomic propositions. Come from the alphabet of
state-machine.
For example, a state S can be {a, b}, which means that a
and b are true in state S, but other atomic propositions are
false.
State S entails atomic-prop a, denoted S |= a, iff a ∈ S
Lev Naiman
CSC410
12/20
Z3
Weakest Precondition
LTL
Definition
Semantics
Proving
LTL
Operators
State S entails boolean formula ϕ if the atomic
propositions it entails imply ϕ
Example: S = {b} then S |= ¬a ∧ b
We have four main LTL operators
: next
♦: eventually
: always
∪: until
Lev Naiman
CSC410
13/20
Z3
Weakest Precondition
LTL
Definition
Semantics
Proving
Outline
1
Z3
Questions
2
Weakest Precondition
Weakest Precondition and Fixed-Points
3
LTL
Definition
Semantics
Proving
Lev Naiman
CSC410
14/20
Z3
Weakest Precondition
LTL
Definition
Semantics
Proving
Semantics
In a syntactic way
We want to define the semantics of LTL in standard first
order logic.
We reference two constants: the path π and start index s.
Let ϕ be a boolean formula, and Φ be an LTL formula.
Let the notation J·K denote semantic interpretation.
Lev Naiman
CSC410
15/20
Z3
Weakest Precondition
LTL
Definition
Semantics
Proving
Semantics
In a syntactic way
Then we define the interpretation of LTL as follows (all
domains for quantifiers are nat):
LTL Semantics
JϕK = πs |= ϕ
JΦK = (λs.JΦK)(s + 1)
J♦ΦK = ∃i.(λs.JΦK)(s + i)
JΦK = ∀i.(λs.JΦK)(s + i)
JΦ0 ∪ Φ1 K = ∃i.(λs.JΦ1 K)(s + i) ∧ ∀j.s ≤ j < i ⇒ (λs.JΦ0 K)(s + j)
Finally, substitute 0 for s as the starting index.
Lev Naiman
CSC410
16/20
Z3
Weakest Precondition
LTL
Definition
Semantics
Proving
Semantics
Examples
Semantically interpret the following LTL formulas: ♦a, ♦a
and prove True ∪ a = ♦a
♦a = ∃i.(λs.πs |= a)(s + i)
= ∃i.πs+i |= a
= ∃i.π0+i |= a
= ∃i.πi |= a
♦a = ∃i.(λs.a)(s + i)
= ∃i.(λs.∀j.(λs.πs |= a)(s + j))(s + i)
= ∃i.∀j.πs+i+j |= a
= ∃i.∀j.πi+j |= a
Lev Naiman
CSC410
17/20
Z3
Weakest Precondition
LTL
Definition
Semantics
Proving
Outline
1
Z3
Questions
2
Weakest Precondition
Weakest Precondition and Fixed-Points
3
LTL
Definition
Semantics
Proving
Lev Naiman
CSC410
18/20
Z3
Weakest Precondition
LTL
Definition
Semantics
Proving
LTL Proofs
Examples
Prove True ∪ a = ♦a
True ∪ a
= ∃i.(λs.πs |= a)(s + i) ∧ ∀j.s ≤ j < i ⇒ (λs.πs |= True)(s + j)
= ∃i.(λs.πs |= a)(s + i) ∧ ∀j.s ≤ j < i ⇒ (λs.True)(s + j)
= ∃i.(λs.πs |= a)(s + i) ∧ ∀j.s ≤ j < i ⇒ True
= ∃i.(λs.πs |= a)(s + i) ∧ True
= ∃i.(λs.JaK)(s + i)
= ♦a
Lev Naiman
CSC410
19/20
Z3
Weakest Precondition
LTL
Definition
Semantics
Proving
LTL Proofs
Examples
There is no need to always semantically expand LTL
formulas for proofs.
Sometimes we can just use the laws of LTL to prove.
Prove that ♦a = ♦ a
♦a
= (True ∪ a)
= True ∪ a
= True ∪ a
=♦a
Lev Naiman
CSC410
20/20
© Copyright 2024 ExpyDoc
