A tiny proof checker in Prolog

The Prolog code for this post is available on GitHub.

I am crazy enough to teach Hoare logic (axiomatic semantics) in the first course for our CS students. For instance, consider the following program (in some simple imperative language), which is supposed to compute quotient q and remainder r according to Euclidian division for operands x and y:

q = 0;
r = x;
while (r >= y) {
   r = r - y;
   q = q + 1; 
}

Given natural numbers x and y, the postcondition of the program is this:

x == q*y + r && q >= 0 && r>=0 && r < y

The precondition is this is:

x >= 0 && y > 0

We are supposed to prove the "triple" consisting of precondition, program, and postcondition.

Let's face it, verification according to Hoare logic is not easily understood by beginners. Many of my students aren't mathematically / logically fit, when they enter the curriculum. So it is a pain in the neck for them to listen and for me to present. However, I think it is still valuable to expose the students to Hoare logic early on, also in the hopes of related topics such as logics and verification to show up again later so that understanding arises through iterations.

So far I have avoided Hoare logic in my course on programming language theory, as I felt that operational and denotational semantics are more presentable in a programming-based fashion. That is, one can obviously write interpreters both in the operational and the denotational style, while the assumption is here that interpreters (say, programs) are easily digested by the average CS student as opposed to proofs and logics.

This time around, I am going to add axiomatic semantics to said course. To this end, I am presenting axiomatic semantics mainly through a simple proof checker that is developed in Prolog. (As reading material I recommend Chapter 6 of Hanne Riis Nielson, Flemming Nielson: Semantics with Applications: A Formal Introduction, Wiley, 1992 because it is easy enough and excellent overall and available online.) In this manner, the programmatic path is also exercised for axiomatic semantics. As a neat side effect, this also allows me to talk about concepts such as rewriting, normalization, simplification, again, in a programming-based fashion. (These concepts are close to my heart as a software language engineer and programming language researchers.)

Here is a quick look at the proof checker.

The rules of Hoare logic are (of course) represented as definite clauses. For example:

/* In the case of an assignment, its precondition is calculated from
 * its postcondition by substituting the LHS variable by the RHS
 * expression.
 */

proof(P, assign(X, E), Q) :-
    subst(Q, X, E, P).

/* In the case of a statement sequence seq(S1, S2), the proof requires
 * subproofs for S1 and S2 subject to an intermediate assertion that
 * serves as postcondition of S1 and precondition of S2. To this end,
 * a statement sequence is represented here as a term with functor
 * seq_/3 (as opposed to the functor seq/2 of the original abstract
 * syntax) so that the extra intermediate assertion can be expressed.
 */

proof(P, seq_(S1, R, S2), Q) :-
    proof(P, S1, R),
    proof(R, S2, Q).

/* In the case of a while-loop while(E, S), the precondition of the
 * loop is per definition the invariant I of the loop and the
 * postcondition must be equivalent to and(I, not(E)). A subproof is
 * due for the body S of the loop such that the invariant follows as
 * postcondition of S for the precondition and(I, E), i.e., the
 * invariant and the loop's condition hold at the beginning of the
 * execution of the body.
 */

proof(I, while(E, S), Q) :-
    sameAs(and(I, not(E)), Q),
    proof(and(I, E), S, I).

/* The precondition of a proof can be strengthened. While
 * simplification/normalization of assertions is performed
 * automatically, strengthening must be explicitly requested. (This is
 * well in line with the usual extra rule of Hoare logic for
 * strengthening the precondition.) In the following notation, we
 * assume pseudo syntax to express the precondition before
 * strengthening, whereas the precondition of the triple is the
 * strengthened one.
 */

proof(P, pre(R, S), Q) :-
    implies(P, R),
    proof(R, S, Q).

subst/4 is substitution of variables by expressions within assertions.
implies/2 is logical implication.
sameAs/2 is equivalence of assertions modulo normalization.
Some rewrite rules of normalization are included for illustration:

% Reflexivity
rewrite(eq(X, X), true).
rewrite(geq(X, X), true).

% Prefer right-associativity over left-associativity
rewrite(and(and(E1, E2), E3), and(E1, and(E2, E3))).
rewrite(or(or(E1, E2), E3), or(E1, or(E2, E3))).

% Unit laws
rewrite(and(true, E), E).
rewrite(and(E, true), E).
rewrite(or(false, E), E).
rewrite(or(E, false), E).
rewrite(add(number(0), X), X).
rewrite(add(X, number(0)), X).

Here is a simple (incomplete) axiomatization of implication:

% Implication complemented by normalization
implies(E1, E2) :-
    normalize(E1, E3),
    normalize(E2, E4),
    implies_(E3, E4).

% Search rules for implication
implies_(E, E).
implies_(_, true).
implies_(and(E1, E2), and(E3, E4)) :-
    implies_(E1, E3),
    implies_(E2, E4).
implies_(and(E1, _), E2) :-
    implies_(E1, E2).
implies_(and(_, E1), E2) :-
    implies_(E1, E2).
implies_(greater(X, number(N1)), greater(X, number(N2))) :-
    N1 > N2.

Here is a simple test predicate for proving correctness of an if-statement:

% Proof for a simple if-statement that computes the max of a and b
prove_if :-
    proof(
     true,
     if(
      greater(var(a), var(b)),
      pre(true, assign(r, var(a))),
      pre(true, assign(r, var(b)))
            ),
     or(eq(var(r), var(a)), eq(var(r), var(b)))
    ).

In abstract syntax, Euclidean division looks like this:

  seq(
    assign(q, number(0)),   
    seq(
      assign(r, var(x)),
      while(
        geq(var(r), var(y)),
        seq(
          assign(r, sub(var(r), var(y))),
          assign(q, add(var(q), number(1)))))))

Here is the proof for Euclidian division; it contains the loop invariant and all other details of the proof.

% Proof for Euclidean division
prove_div :-
    proof(

      % "As declared" precondition of the program
      % x >= 0 && y > 0
      and(
        geq(var(x), number(0)), % As computed
        greater(var(y), number(0))), % Vacuously added for division by zero

      % Strengthen precondition
      pre(

        % Computed (weakest) precondition of the program
        geq(var(x), number(0)),

        % Beginning of program code
        seq_(

          % q = 0;
          assign(q, number(0)),   

          % Intermediate assertion
          and(
            eq(var(x), add(mul(var(q), var(y)), var(x))),
            and(
              geq(var(q), number(0)),
              geq(var(x), number(0)))),
    
          seq_(

            % r = x;
            assign(r, var(x)),
    
            % Intermediate assertion = invariant for while loop
            and(
              eq(var(x), add(mul(var(q), var(y)), var(r))),
              and(
                geq(var(q), number(0)),
                geq(var(r), number(0)))),

            while(
     
              % Loop condition                     
              geq(var(r), var(y)),
     
              % Strengthen precondition
              pre(
    
                % Computed precondition of body
                and(
                  eq(var(x), add(mul(add(var(q), number(1)), var(y)), sub(var(r), var(y)))),
                  and(
                    geq(add(var(q), number(1)), number(0)),
                    geq(sub(var(r), var(y)), number(0)))),
    
                % Loop body
                seq_(
     
                  % r = r - y;
                  assign(r, sub(var(r), var(y))),

                  % Intermediate assertion
                  and(
                    eq(var(x), add(mul(add(var(q), number(1)), var(y)), var(r))),
                    and(
                      geq(add(var(q), number(1)), number(0)),
                      geq(var(r), number(0)))),
     
                  % q = q + 1;
                  assign(q, add(var(q), number(1))))))))),

      % "As declared" postcondition of the program
      % x == q*y + r && q >= 0 && r>=0 && r < y
      and(
        eq(var(x), add(mul(var(q), var(y)), var(r))),
        and(
          geq(var(q), number(0)),
          and(
            geq(var(r), number(0)),
            not(geq(var(r), var(y))))))
    ).

It just works:

?- prove_div.
true