CS709 - Formal Methods For Software Engineering Course Page Mcqs Q & A Video Downloads Short Question & Answers     Q1: Solve using logical equivalence p=q=true=p
Fall 2016 – Mid
p=q=true=p
≡ p=p=true=q
≡ true=q
≡ q
Q2: Simplify p ≢ q ≡ r ≡ p
Fall 2016 – Mid

Q3: Find WP(x:= 3*y+5, x:=11)
Fall 2016 – Mid
WP(x:= 3*y+5, x:=11)
== 3*y+5 = 11
== 3y = 6
== y = 2
Q4: Statement: X, y:=x-y, x+y      Post-Condition: xy = 1
Calculate pre-condition and also simplify it
Fall 2016 – Mid
WP(y:=x-y, x+y, xy=1)
== wp(y:=x-y, wp(x+y, xy=1))
== wp(y:=x-y, wp(x=-y, xy=1))
== wp(y:=x-y, -2y=1))
== -2*(x-y) = 1
== -2x + 2y = 1
== 2y = 2x + 1
== y = x + ½
Q5: Find Weakest precondition of
WP( i = i + 1; j = j + 1; i = j )
Fall 2016 – Mid
wp( i = i + 1; j = j + 1; i = j )
:= wp(i=i+1, wp(j=j+1, i=j))
:=wp(i=i+1, i=j+1)
:= i+1=j+1
:= i=j
Q6: Simply with triple Hoarse logic and tells whether it is INVALID or INVALID hoarse logic? {false} i:=1 {i=0}
Fall 2016 – Mid
~impossible, 1 cannot be equal to 0, prove

The function gets the false value as an input, if it is so, we can infer anything, whatever the value is. The output will be only false, an error command, a contradiction. When the function takes the false value as an input, after executing the program statement, i.e. the value of i changes 1 to 0 as an output.
WP(i:=1, i:=0)
:= i = 0   // an output, where i = 1
:= 1 = 0 // ~impossible
Q7: Write Weakest Precondtion of:
i) WP(i,j:=i+1,j+i,i=j)
ii) WP(a,b>5,b=a)
Fall 2016 – Mid
i) WP(i,j:=i+1,j+i,i=j)
≡ i + j = 0

ii) WP(a,b>5,b=a)
≡ wp(a, wp(b>5, b=a))
≡ wp(a, a>5)
≡ a>5
Q8: According to hoare triple, are both valid or invalid?
i=0, i=j+1. {i>j}
i=0, i=j+1. {i<i}
Fall 2016 – Mid
since i=j+1 in both cases, when the set of statement execute,
i=0, i=j+1. {i>j} // correct
i=0, i=j+1. {i<i} // incorrect
Q9:Simplify the given: p=q=p=q=p=q=p
Fall 2016 – Mid
p=q=p=q=p=q=p
≡ p=p=p=p=q=q=q
≡ true=true=true=q
≡ true=true=q
≡ true=q
≡ q
Q10: Logical Equivulences Chart      Course Instructorr Dr. Fakhar Lodhi D.Sc. Computer Science George Washington University, USA. Javascript is disable - Webestools - Vote Service (notation module) Books Design by contract by example by Richard Mitchell and Jim McKim Object-Oriented Software Construction by Bertrand Meyer Program Construction and Verification by Roland C. Backhouse Program Construction: Calculating Implementation by Roland Backhouse Software Engineering by Ian Sommerville The Object Constraint Language, precise modeling with UML by Jos Warmer and Anneke Kleppe The Specification of Complex Systems by B. Cohen, W. T. Harwood and M. I. Jackson Using Z: Specification, Refinement, and Proof by Jim Woodcock & Jim Davies