University Jena, Department of Mathematics & Computer Science
Programming Languages and Compilers

Best viewed with Netscape 2 or 3. For fixed font use Courier New 9 pts


Frege Program Prover (FPP): Examples

  • Example 1: lexical error
  • Example 2: syntax error
  • Example 3: assignment statement
  • Example 4: inconsistent program
  • Example 5: if statement
  • Example 6: case statement
  • Example 7: for statement
  • Example 8: while statement
  • Example 9: wp computation
  • Example 10: proving an implication
  • Example 1: lexical error

    input

    --!pre: true;
    x := 1;
    --!post: x != 0;
    output

    --!pre: true;
    x := 1;
    --!post: x != 0;?? lexical error!??
      top of page

    Example 2: syntax error

    input

    --!pre: true;
    x := ;
    --!post: x /= 0;
    output

    --!pre: true;
    x := ;
    Error ^ inserted token NULL_TOKEN
    --!post: x /= 0;
    Ayacc.YYParse : 1 syntax error found.
      top of page

    Example 3: assignment statement

    input

    --!pre: true;
    x := 1;
    --!post: x /= 0;
    output

    --!pre : true;
    --> wp : (1) /= 0;
    --> vc : [(true) => ((1) /= 0)];
    --> result: proved
    x := 1;
    --!post : x /= 0;
      top of page

    Example 4: inconsistent program

    input

    --!pre:-128 <= X AND X <= 127 AND X = Kx ;
    x := -x;
    --!post: -128 <= X AND X <= 127 AND X = -Kx;
    output

    --!pre : (-128 <= x AND x <= 127 AND x = kx)
    --> wp : -128 <= -x AND -x <= 127 AND -x = -kx)
    --> vc : (-128 <= x AND x <= 127 AND x = kx)
    --> ==> (-128 <= -x AND -x <= 127 AND -x = -kx)
    --> result: not proved
    --> Incorrectness condition: (-127 - kx >= 1 AND
    --> 127 - kx >= 0 AND
    --> 128 + kx >= 0)
    x := -x;
    --!post : (-128 <= x AND x <= 127 AND x = -kx)
      top of page

    Example 5: if statement

    input

    --!pre: x=a;
    if x<0
       then x := -x;
    end if;
    --!post: (a >= 0 and x = a)
          or (a < 0 and x = -a);
    output

    --!pre       : x = a 
    --> wp       :     0 >= 1 + x AND (a >= 0 AND -x = a OR 0 >= 1 + a AND -x = -a)
    -->             OR 0 <= x AND (a >= 0 AND x = a OR 0 >= 1 + a AND x = -a) 
    --> vc       :      x = a 
    -->            ==>          0 >= 1 + x 
    -->                     AND a >= 0 AND -x = a OR 0 >= 1 + a AND -x = -a 
    -->                 OR 0 <= x AND (a >= 0 AND x = a OR 0 >= 1 + a AND x = -a) 
    --> Result: proved 
    IF x < 0 THEN  
       x := -x; 
    end if; 
    --!post      : a >= 0 AND x = a OR 0 >= 1 + a AND x = -a 
      top of page

    Example 6: case statement

    input

    --!pre: c>0;
    case x is
         when -c..-1 => z := -x;
         when 1..c   => z := x;
         when others => z := 1;
    end case;
    --!post: z>=0;
    output

    --!pre       : c >= 1 
    --> wp       :    -c <= x AND x <= -1 AND -x >= 0 
    -->            OR 1 <= x AND x <= c AND x >= 0 
    -->            OR (-c >= 1 + x OR x >= 0) AND (1 >= 1 + x OR x >= 1 + c) 
    --> vc       :      c >= 1 
    -->            ==>     -c <= x AND x <= -1 AND -x >= 0 
    -->                 OR 1 <= x AND x <= c AND x >= 0 
    -->                 OR (-c >= 1 + x OR x >= 0) AND (1 >= 1 + x OR x >= 1 + c) 
    --> Result: proved 
    case x is 
       when -c .. -1 => 
          z := -x; 
       when 1 .. c => 
          z := x; 
       when others => 
          z := 1; 
    end case; 
    --!post      : z >= 0
      top of page

    Example 7: for statement

    input

    --!pre: n>=0;
    s := 0;
    --!pre: s=0 and n>=0;
    --!post: s=sum(k,k,1,n);
    --!inv: s=sum(k,k,1,i);
    for i in 0..n loop
         s := s+i;
    end loop;
    output

    --!pre       : n >= 0 
    --> wp       : n >= 0 
    --> vc       : True 
    --> Result: proved 
    s := 0; 

    --!pre       : s = 0 AND n >= 0 
    --!post      : s = sum(k,(k,1,n)) 
    --!inv       : s = sum(k,(k,1,i)) 
    -->functionality --------------------------- 
    -->func      : (initial AND induction AND final AND null loop) 
    -->initial   :0 <= n AND s = 0 AND n >= 0 ==> s = 0 
    --> Result    : proved 
    -->induction :0 <= n AND s = sum(k,(k,1,-1 + i)) ==> i + s = sum(k,(k,1,i)) 
    --> Result    : proved 
    -->final     :0 <= n AND s = sum(k,(k,1,n)) ==> s = sum(k,(k,1,n)) 
    --> Result    : proved 
    -->null loop :0 >= 1 + n AND s = 0 AND n >= 0 ==> s = sum(k,(k,1,n)) 
    --> Result    : proved 
    for i in 0 .. n  loop 
       s := s + i; 
    end loop; 
      top of page

    Example 8: while statement

    input

    --!pre: i>0 and j>0 and
       i=k1 and j=k2;
    --!post: i=j and i=GGT(k1,k2);
    --!inv: i>0 and j>0 and
       GGT(i,j) = GGT(k1,k2);
    --!term: i+j;
    while i /= j loop
         if i>j then i := i-j;
         else j := j-i;
         end if;
    end loop;
    output

    --!pre       : i >= 1 AND j >= 1 AND i = k1 AND j = k2 
    --!post      : i = j AND i = GGT(k1,k2) 
    --!inv       : i >= 1 AND j >= 1 AND GGT(i,j) = GGT(k1,k2) 
    --!term      : j + i 
    -->functionality --------------------------- 
    -->initial   :     i >= 1 AND j >= 1 AND i = k1 AND j = k2 
    -->            ==> i >= 1 AND j >= 1 AND GGT(i,j) = GGT(k1,k2) 
    --> Result    : proved 
    -->induction :     i /= j AND i >= 1 AND j >= 1 AND GGT(i,j) = GGT(k1,k2) 
    -->            ==>          i >= 1 + j 
    -->                     AND -j + i >= 1 
    -->                     AND j >= 1 
    -->                     AND GGT(i,j) = GGT(k1,k2) 
    -->                 OR      i < 1 + j 
    -->                     AND i >= 1 
    -->                     AND j - i >= 1 
    -->                     AND GGT(i,j) = GGT(k1,k2) 
    --> Result    : proved 
    -->final     :     i = j AND i >= 1 AND j >= 1 AND GGT(i,j) = GGT(k1,k2) 
    -->            ==> i = j AND i = GGT(k1,k2) 
    --> Result    : proved 
    -->termination --------------------------- 
    -->initial   :     i /= j AND i >= 1 AND j >= 1 AND GGT(i,j) = GGT(k1,k2) 
    -->            ==> j + i >= 1 
    --> Result    : proved 
    -->induction :     i /= j AND i >= 1 AND j >= 1 AND GGT(i,j) = GGT(k1,k2) 
    -->            ==>     i >= 1 + j AND j + i >= 1 + i 
    -->                 OR i < 1 + j AND j + i >= 1 + j 
    --> Result    : proved 
    while i /= j loop 
       IF i > j THEN  
          i := i - j; 
       ELSE 
          j := j - i; 
       end if; 
    end loop;
      top of page

    Example 9: wp computation

    input

    if a /= 0
    then q := q/a;
    elsif q>0
    then q := -q;
    else q := 0;
    end if;
    --!post: q*a > 0;
    output

    --> wp       : a /= 0 AND q >= 1 OR a = 0 AND q >= 1 AND -(a*q) >= 1 
    IF a /= 0 THEN  
       q := q / a; 
    ELSIF q > 0 THEN  
       q := -q; 
    ELSE 
       q := 0; 
    end if; 
    --!post      : a*q >= 1
      top of page

    Example 10: proving an implication

    input

    --!pre: x <= y;
    null;
    --!post: x = min(x,y);
    output

    --!pre : x <= y;
    --> wp : x = min(x, y);
    --> vc : [(x <= y) => (x = min(x, y))];
    --> result: proved
    null;
    --!post : x = min(x, y);
      top of page