Formal Methods in Software Engineering 2008, Summer school

Propositional Logic

• no, reallySimple.key (doesn't close) ==> true -> p
• doubleNegation ==> (A -> B) -> !!(A -> B)
  show rule sequence: "nnf_imp2or, orRight, notRight" versus "impRight"
• contraPosition ==> (p -> q) -> !q -> !p
  show "replaceKnownLeft" and "replaceKnownRight" rules
• liarsville.
  Early proof splitting creates large proof. Instead apply local transformations and use the "replaceKnownLeft" and "replaceKnownRight" rules.
• AllClausesLength4
  • Apply 16 automatic rules to do "andLeft" automatically
  • Use the cut rule on a. Apply 60 Rules.
  • Use cut rule on b and so on with 30 rules

Predicate Logic

• pred0.key ==> a = b & b = c -> a = c
• pred1.key ==> \exists s x; \forall s y; p(x, y) -> \forall s v; \exists s u; p(u, v)
• pred2.key ==> \forall s x; f(g(x)) = g(x) & g(a) = b -> f(b) = g(a)
• pred3.key : transitive & ireflexive -> asymetric \forall s x; \forall s y; \forall s z; ((p(x, y) & p(y, z) -> p(x, z)) & !p(x, x)) ==> \forall s x; \forall s y; (p(x, y) -> !p(y, x))
• exist1.key ==> \exists s x; \exists s y; (p(x, y) <-> p(y, x)) - use META VARIABLES
• pred4.key \exists z x; \exists z y; p(x, y) & \forall z x; !p(x, x) -> \exists z x; \exists z y; !x = y - You can use meta-variables
• pred5.key \exists z x; \exists z y; (p(x, y) & !p(y, x)) -> \exists z x; \exists z y; !x = y - you can use meta-variables
• pred6.key

  	\forall person x;  (!liar(x) <-> honest(x)),
  	honest(a),
  	liar(b),
  	honest(c),
  	honest(d),
  	liar(e)
  	==>
  	(honest(a) -> (liar(b) <-> honest(d)))
  	& (honest(b) -> honest(c) -> liar(a) | liar(d))
  	& (honest(c) -> liar(e))
  	& (honest(c) -> liar(a) | liar(b))
  	& (honest(d) -> honest(b) -> liar(a) | liar(c))
  	& (honest(e) -> \exists person y;  (!y = b & !y = e -> liar(y)))
  

• functions.key ==> \forall s x; f(g(x)) = g(x) & g(a) = b -> f(b) = g(a)
• count.key ==> \forall int x; (p(x) -> p(x + 1)) & p(0) -> p(2)
• count2.key ==> \forall s x; x = f(x) & a = b -> f(f(f(f(a)))) = b
• count3.key ==> \forall s x; g(x) = f(g(x)) & g(g(a)) = z -> f(g(f(g(a)))) = z

Predicate Logic with integer arithmetics

• binomial1.key ==> \forall int a; \forall int b; (a + b) * (a + b) = a * a + 2 * a * b + b * b
• binomial2.key ==> \forall int a; \forall int b; (a + b) * (a - b) = a * a - b * b
• equalities2.key ==> 5 = a & 15 = b + -3 -> a * b = 90
• equalities3.key ==> 5 = a & 15 + (3 + -a) = b -> a * b = 65
• subsumptionExample.key ==> a >= 13 -> !5 * a < 50
• inequations2.key ==> a + b <= 5 & a >= 0 & a - 2 * b <= -20 -> false

Simple Dynamic Logic

• helloWorld1.key \<{ int hello = 1; int world = 2; int helloWorld = hello+world; }\> helloWorld = hello + world - Shows execution with concrete values. The update represents the memory.
• helloWorld2.key \<{ int hello; int world; int helloWorld = hello+world; }\> helloWorld = world + hello - Symbolic execution. Update represents memory with abstract values.
• helloWorld3.key - Execution of an IF-statement with concrete values
• helloWorld4.key - Quantification on program variables. Symbolic execution of IF-statement is abstract values.
• complex.key ==> \<{ int i = 0; if ((i=2)>=2) { i++;}}\> i = 3
• p17_1.key i = a ==> \<{ i++; }\> i = a + 1
• p17_1b_OF.key
  
  • The example is:i <= 2147483647 & i > 0 & i = a ==> \<{i++;}\> i = a + 1
  • First turn off Overflow semantics. The example can be proved. But this is unsound
  • Turn on Overflow semantics. The example is not provable due to overflow
  • Explain the conversion from javaAddInt((jint)(0), 1) to \if (inInt((jint)(0) + 1)) \then ((jint)(0) + 1) \else (javaAddIntOverFlow((jint)(0), 1))
• p17_1b.key
  • i < 2147483647 & i > 0 & i = a ==> \<{i++;}\> i = a + 1
  • Provable with activated overflow checking.
• p17_2.key \<{if (k==0) {i=k;} else {i=0;}}\> i = 0

Java Card DL

• Turn off null checking.
• alias1IngnoreNullCheck.key - not provable because of aliasing.
• alias2IngnoreNullCheck.key - fixed aliasing.
  provable with NullCheck off.
• alias3IngnoreNullCheck.key
  - Delayed Update application
• updatesimplifier.key

  \<{MyClass o; MyClass p; p=o.a; o.a=o; }\> o.a.a.a.a.b = o.b

• method.key - Turn OFF Overflow Checking

  ==> \forall int i; {p.age:=i}
  	 (i >= 0 -> \<{p.birthday();}\> p.age = i + 1)
  	

• method2.key - Shows parameter handling
• instanceCreation.key
• Turn ON NullChecking. And reload alias3IngnoreNullCheck.key
  You get a NullPointerException
  
• alias4WithNullCheck.key - with NullChecking ON
• p17_3XXX.key
• p17_3.key - NullChecking OFF

JML - Finite Loops - Method Contracts

• JavaCardDL/classes/C.java - write class with a method with a finite loop and JML: incLoop

  /*@ public normal_behavior
  	requires y==2;
  	assignable \nothing;
  	ensures \result==x*y;@*/
   public int incLoop(int x, int y){
  	int tmp=0;
  	while(y>0){tmp += x;y--;}
  	return x;
   }
  

• write a method that calls incLoop and then show methodContract rule

  public int val;
  /*@ public normal_behavior
  	requires 0<val && val <1000;
  	assignable val;
  	ensures val == \old(val) * 2 && val>0;
  @*/
   public int doubleVal(){
  	val = incLoop(val, 2);
   }
  

Loop Invariant

• {_old21_y:=2 }
     \<{method-frame(result->_jmlresult96, source=C,this=self_C): {
           while ( y>0 ) {
             tmp+=x;
             y--;
           }
               return  tmp;
         }
       }\> _old21_y * _old20_x = _jmlresult96

  
  The loop invariant is:y>=0 & (_old21_y - y) * x = tmp