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 2025 ExpyDoc