CORE AXIOMATIC SEMANTICS CODED IN PROLOG
                              ----------------------------------------


          Script started on Tue Oct 11 14:30:19 1994

          vestavia% cat coreas.pro
          /* set up program to be verified, pre-condition, post-condition and */
          /* loop invariant                                                   */

          program(:(
                    :(
                      :=(q, 0),
                      :=(r, x)),
                    while_loop(>=(r, y),
                      :(
                        :=(q, +(q, 1)),
                        :=(r, -(r, y)))))).

          pre_condition(and(>=(x, 0), >(y, 0))).

          post_condition(and(=(x, +(*(q, y), r)), not(>=(r, y)))).

          loop_invariant(and(=(x, +(*(q, y), r)), >=(r, 0))).

          /* axiomatic semantics */

          verify(P, :(S1, S2), R) :- verify(Q, S2, R), verify(P, S1, Q).

          verify(P, input(and(W1, W2)), Q) :- verify(P, :(input(W1), input(W2)), Q).

          verify(P, output(and(W1, W2)), Q) :- verify(P, :(output(W1), output(W2)), Q).

          verify(and(=(input_file, [K | L]), P1), input(V), and(=(input_file, L), P)) :-
              subst(P, K, V, P1).

          verify(and(and(=(output_file, L), P), =(V, K)), output(V),
                  and(and(=(output_file, L1), P) =(V, K))) :-
              append(L, K, L1).

          verify(P1, :=(V, E), P) :- subst(P, E, V, P1).

          verify(P, if_then(B, S), Q) :-
              verify(and(P, B), S, Q), implies(and(P, not(B)), Q).

          verify(P, if_then_else(B, S1, S2), Q) :-
              verify(and(P, B), S1, Q), verify(and(P, not(B)), S2, Q).

          verify(P, while_loop(B, S), and(P, not(B))) :-
              loop_invariant(P), verify(and(P, B), S, P).

          verify(P, S, R) :- implies(Q, R), verify(P, S, Q).

          verify(P, S, R) :- implies(P, Q), verify(Q, S, R).

          verify(and(P, P1), S, and(Q, Q1)) :- verify(P, S, Q), verify(P1, S, Q1).

          verify(or(P, P1), S, or(Q, Q1)) :- verify(P, S, Q), verify(P1, S, Q1).








          /* variable substitution rules */

          subst(and(P1, P2), E, V, and(Q1, Q2)) :-
              subst(P1, E, V, Q1), subst(P2, E, V, Q2).

          subst(or(P1, P2), E, V, or(Q1, Q2)) :-
              subst(P1, E, V, Q1), subst(P2, E, V, Q2).

          subst(not(P), E, V, not(Q)) :- subst(P, E, V, Q).

          subst(=(E1, E2), E, V, =(E3, E4)) :-
              subst(E1, E, V, E3), subst(E2, E, V, E4).

          subst(<>(E1, E2), E, V, <>(E3, E4)) :-
              subst(E1, E, V, E3), subst(E2, E, V, E4).

          subst(<(E1, E2), E, V, <(E3, E4)) :-
              subst(E1, E, V, E3), subst(E2, E, V, E4).

          subst(<=(E1, E2), E, V, <=(E3, E4)) :-
              subst(E1, E, V, E3), subst(E2, E, V, E4).

          subst(>(E1, E2), E, V, >(E3, E4)) :-
              subst(E1, E, V, E3), subst(E2, E, V, E4).

          subst(>=(E1, E2), E, V, >=(E3, E4)) :-
              subst(E1, E, V, E3), subst(E2, E, V, E4).

          subst(+(E1, E2), E, V, +(E3, E4)) :-
              subst(E1, E, V, E3), subst(E2, E, V, E4).

          subst(-(E1, E2), E, V, -(E3, E4)) :-
              subst(E1, E, V, E3), subst(E2, E, V, E4).

          subst(*(E1, E2), E, V, *(E3, E4)) :-
              subst(E1, E, V, E3), subst(E2, E, V, E4).

          subst(V, E, V, E) :- atom(V).

          subst(V1, E, V, V1) :- atom(V1), not(equal(V, V1)).

          subst(N, E, V, N) :- number(N).

          /* logical implications rules (for this example only!) */

          implies(and(>=(x, 0), >(y, 0)), and(=(x, +(*(0, y), x)), >=(x, 0))).
          implies(and(and(=(x, +(*(q, y), r)), >=(r, 0)), >=(r, y)),
              and(=(x, +(*(+(q, 1), y), -(r, y))), >=(-(r, y), 0))).
          implies(and(and(=(x, +(*(q, y), r)), >=(r, 0)), not(>=(r, y))),
              and(=(x, +(*(q, y), r)), not(>=(r, y)))).

          /* equality predicate */

          equal(X, X).








          vestavia% sbprolog
          SB-Prolog Version 3.1
          | ?- consult('coreas.pro').
          yes
          | ?- pre_condition(P), program(S), post_condition(Q), loop_invariant(I),
                   verify(P, S, Q).

          P = and(x >= 0,y > 0)
          S = :(:(:=(q,0),:=(r,x)),while_loop(r >= y,:(:=(q,q + 1),:=(r,r - y))))
          Q = and(x = q * y + r,not r >= y)
          I = and(x = q * y + r,r >= 0)
          yes
          | ?- ^D
          Halt. Program terminated normally

          vestavia% ^D
          script done on Tue Oct 11 14:32:07 1994