George: User Manual

A program correctness proof consists of an annotated program and proofs in natural deduction of any verification conditions generated by the annotated program.

A program consists of a sequence of functions and procedures. Here is the syntax for each of the programming constructs in our little programming language:

proc (optional list of args) { ... }	fun (optional list of args) { ... }
if B then { ... };	if B then { ... } else { ... };
while B do { ... };	V := E;

A program assertation (a wff about the program variables) can be inserted between any lines of a program. A program assertion is of the form "assert( wff )" where wff is any formula in predicate logic with set theory.

Program correctness rule names should follow all the assertions (except the first one in a function/procedure) using the syntax in "assert( P ) by rule_name;".

Functions must have a return statement of the form "return x;" where "x" is any variable name. This statement must be second-last in the body of the function (last is the postcondition assertion).

#check PC

// fact(x) means x!  (i.e., factorial)

proc main(x) {
         assert(true);
        assert(1 = fact(0)) by implied on VC1;
    y := 1;
        assert(y = fact(0)) by asn;
    z := 0;
        assert(y = fact(z)) by asn;
    while !(z = x) do {
            assert( y = fact(z) & !(z = x) ) by partial_while;
            assert( (z+1)*y = fact(z+1) ) by implied on VC2;
        z := z + 1;
            assert( z * y = fact(z) ) by asn;
        y := z * y;
            assert( y = fact(z) ) by asn;
    };
        assert( y = fact(z) & z = x ) by partial_while;
        assert( y = fact(x) ) by implied on VC3;
}

#check ND

// VC 1

true
|-
1 = fact(0)

1) true  premise
2) 1 = fact(0) by arith

#check ND

// VC 2

y = fact(z) & !(z = x) 
|-
(z+1)*y = fact(z+1)

1) y = fact(z) & !(z = x)     premise
2) y = fact(z)                 by and_e on 1
3) (z+1)*y = (z+1)* fact(z)    by arith on 2
4) (z+1)*y = fact(z+1)         by arith on 3 // and defn of ! 

#check ND

// VC 3

y = fact(z) & z = x
|-
y = fact(x)

1) y = fact(z) & z = x premise
2) y = fact(z)          by and_e on 1
3) z = x                by and_e on 1
4) y = fact(x)          by eq_e on 2,3

#check PC

fun find(B, i, c) {
         assert(exists k . 0 <= k & k <= i & (B[k] = c) );
    if (B[i] = c) then {
            assert( (exists k . 0 <= k & k <= i & (B[k] = c)) & B[i] = c ) by if_then_else;
            assert( B[i] = c ) by implied on VC1;
        ret := i;
            assert( B[ret] = c ) by asn;
    } else {
            assert( (exists k . 0 <= k & k <= i & (B[k] = c)) & !(B[i] = c) ) by if_then_else;
            assert( B[find(B, i-1, c)] = c ) by implied on VC2;
        ret := find(B, i-1, c);
            assert( B[ret] = c ) by asn;
    };
    return ret;
        assert( B[ret] = c ) by if_then_else;
}

/*
Base case: The base case is when B[i] = c, which satisfies the precondition
exists k . 0 <= k & k <= i & (B[k] = c).  In this case, a trace of the program leaves
ret = i at the end of the function, which satisfied the postcondition because
B[ret] = c
*/


#q VC1

#check ND

(exists k . 0 <= k & k <= i & (B[k] = c)) & B[i] = c
|-
B[i] = c

1) (exists k . 0 <= k & k <= i & (B[k] = c)) & B[i] = c premise
2) B[i] = c by and_e on 1

#q VC2

#check ND

// The first premise is from the fcn rule.

(exists k. 0 <= k & k <= i - 1 & B[k] = c) => B[find(B, i-1, c)] = c,  // by the fcn rule
(exists k . 0 <= k & k <= i & (B[k] = c)) & !(B[i] = c)
|-
B[find(B, i-1, c)] = c

lem1) (exists k. 0 <= k & k <= i - 1 & B[k] = c) => B[find(B, i-1, c)] = c premise 

1) (exists k . 0 <= k & k <= i & (B[k] = c)) & !(B[i] = c)     premise
2) exists k . 0 <= k & k <= i & (B[k] = c)                      by and_e on 1
3) !(B[i] = c)                                             by and_e on 1
4) for some ku assume 0 <= ku & ku <= i & (B[ku] = c) {
    5) 0 <= ku              by and_e on 4
    6) ku <= i              by and_e on 4
    7) B[ku] = c           by and_e on 4
    8) disprove ku = i {
        9) B[i] = c        by eq_e on 7,8
        10) false           by not_e on 3,9
    }
    11) !(ku = i)                              by raa on 8-10
    12) ku <= i-1                               by arith on 6,11
    13) 0 <= ku & ku <= i-1                     by and_i on 5,12
    14) 0 <= ku & ku <= i-1 & B[ku] = c        by and_i on 13, 7
    15) exists k. 0 <= k & k <= i - 1 & B[k] = c    by exists_i on 14
}
16) exists k. 0 <= k & k <= i - 1 & B[k] = c        by exists_e on 2, 4-15
17) B[find(B, i-1, c)] = c                           by imp_e on lem1, 16

What does george check?

#check PCrun and #check PCrunVerbose do what #check PC does but additionally evaluate whether each assertion is valid during the execution of the program and provide different amounts of output to help debug these assertions. For example, these commands can help you see if your chosen loop invariant stay true throughout the execution of a loop.

Output is limited to a certain number of lines, assertions are true unless feedback indicates otherwise (in non-verbose mode), and the quantification over integers is limited to 0-maximum. These limits can be changed if the need arises. There is also a limit on the number of loop iterations to avoid infinite loops. Formula labels cannot be used when using PCrun or PCrunVerbose.

To use #check PCrun and #check PCrunVerbose all variables must be initialized within the program before the precondition (since we have no input/output statements and the precondition must be true to proceed with the program!). This initialization is not required in program correctness proofs in general.

#check PCrun shows the values of variables at the beginning of loops only whereas #check PCrunVerbose shows the values of variables after every statement.

Logical operators are evaluated lazily to avoid problems with undefined elements of arrays.

george: User Manual

Program Correctness (#check PC, #check PCrun, #check PCrunVerbose)

What does george check?