Lösungsvorschlag Formal Methods Endterm 2011

Aus VISki
Wechseln zu: Navigation, Suche

Assignment 1

Abbreviations:

  • s:
 r := 1;
 while j > 1 do
   r := r * j;
   j := j - 1;
 end
  • l:
 while j > 1 do
   r := r * j;
   j := j - 1;
 end
  • l' :
 r := r * j;
 j := j - 1;
  • [2,0] =

Derivation Sequence:

  1. 〈s, [3]〉→₁
  2. 〈r := 1; l, [3]〉→₁
  3. 〈l, [3, 1]〉→₁
  4. 〈if j > 1 then l';l else skip end, [3, 1]〉→₁
  5. 〈r := r * j; j := j - 1; l, [3, 1]〉→₁
  6. 〈j := j -1; l, [3, 3]〉→₁
  7. 〈l, [2, 3]〉→₁
  8. 〈if j > 1 then l'; l else skip end, [2, 3]〉→₁
  9. 〈r := r * j; j := j - 1; l, [2, 3]〉→₁
  10. 〈j := j - 1; l, [2, 6]〉→₁
  11. 〈l, [1, 6]〉→₁
  12. 〈if j > 1 then l'; l else skip end, [1, 6]〉→₁
  13. 〈skip. [1, 6]〉→₁
  14. 〈[1, 6]〉

Assignment 2

Invariant:

Proof outline




 i := n




 sum := 0



 while i # 0 do



   sum := sum + i;

   i := i - 1;

 end



Assignment 3

Claim:

Proof of ""

  • I'll do a proof by induction on the shape of the inference tree of .
  • Out of the six rules of axiomatic semantics, only WH_Ax or CONS_Ax can be at the root of the tree
  • Case WH_Ax:
    • The rule is as followed defined,

hence: , thus:

  • Case CONS_Ax:
    • From CONS_Ax we know, there exists an inference tree for , where
    • By applying the induction hypothesis to , we get
    • Because we have and , we can build following chain of implications: . And we are done.
    • Old Version: by applying the induction hypothesis to , we get
    • Old Version: Now we have thus

Proof of ""

Direct proof, i.e. we assume for arbitrary and show .

We can construct a derivation tree for as follows:

QED

Assignment 4

Task A

Claim:

Proof (by strong induction on , i.e. the length of the derivation sequence):

Induction hypothesis:

Let be arbitrary.

  • Case
    • If the implication holds trivially since there is no derivation sequence of length from a non-final state into a final state in the SOS.
  • Case
    • For this case we proceed by a direct proof, i.e. we assume, for an arbitrary , that holds and then show that also holds.
    • There are two possible rules which can have been applied at the root:
      • Case
        • From the rule follows: for some state
        • The first transition is justified by the following derivation tree:
        • From this we can construct the following derivation tree using the rule :
        • Putting all together we get:
        • So holds
      • Case
        • From the rule follows: for some statement and some state
        • The first transition is justified by the following derivation tree:
        • From this we can construct the following derivation tree using the rule :
        • By applying the induction hypothesis on the second transition, i.e. on , we get (possible because and because is for sure greater or equal to 0):
        • Putting all together yields
        • So holds

QED


Task B

let be

(1) x = x + 1;
(2) x = x * 2;

and

(3) x = x + 2;
(4) x = x * 3;

and
then by applying first PAR1_SOS, then PAR3_SOS and repeating these two steps (doing lines 1-3-2-4 in that order), we reach the state , which is not reachable from either 〈〉 nor 〈

Assignment 5

Task A

active proctype client (int address; mtype language) {
    request req;
    req.address = address;
    req.language = language;
    answer ans;
    answer dummy;
    dummy.address = -1;
    dummy.data = 0;
    net ! dummy, req;
    net ? (ans, _);
    do
    :: ans.address != address -> net ! dummy, req;
                                 net ? (ans, _);
    :: else -> break
    od                                                                                                               
}  

Task B

active proctype server() {                                                                                           
    request req;                                                                                                     
    request dummy;                                                                                                   
    dummy.address = -1;                                                                                              
    dummy.language = de;                                                                                             
    answer ans;
    do
    :: net ? (_, req);
       if
       :: req.language == de -> ans.data = msg_de;
                                nreq_de = nreq_de + 1;
                                ans.address = req.address;
                                net ! ans, dummy;
       :: else -> ans.data = msg_en;
                  nreq_en = nreq_en + 1;
                  ans.address = req.address;
                  net ! ans, dummy;
       fi
    od
}

Task C

  • It is a liveness property. For any prefix of a trace there exists a infinite continuation (the one that answers all remaining queries) that satisfies the property.
  • request_m answer_m