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.
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