hoare.pl

hoare.pl

:- initialization(main).
:- op(800,xfy,['or','&&']).

% proof/3 は proof({P};U;{Q}) 状態PがUを実行するとQに成るという意味。

proof({P}; skip(); {Q}) :- sameAs(P, Q). % スキップは何も変わらない
proof({P}; X = E; {Q}) :- subst(Q, X, E, P). % 代入はsubstを実行する
proof({P}; (S1; {R}; S2); {Q}) :- proof({P}; S1; {R}), proof({R}; S2; {Q}). % セミコロンは途中にもある
proof({P}; if(E, S1, S2); {Q}) :- proof({P && E}; S1; {Q}), proof({P && not(E)}; S2; {Q}).
proof({I}; while(E; S); {Q}) :- sameAs(I && not(E), Q), proof({I && E}; S; {I}).
proof({P}; ({R}; S); {Q}) :- implies(P, R), proof({R}; S; {Q}).
proof({P}; (S; {R}); {Q}) :- implies(R, Q), proof({P}; S; {R}).

subst(E1, X, E2, E3) :- subst_(E1, X, E2, E4), sameAs(E3, E4).
subst_(N, _, _, N) :- integer(N).
subst_(X, X, E, E) :- val(X).
subst_(X1, X2, _, X1) :- val(X1), \+ X1 == X2.
subst_(not(E1a), X, E0, not(E2a)) :- subst_(E1a, X, E0, E2a).
subst_(E1, X, E0, E2) :-
    E1 =.. [F, E1a, E1b], E2 =.. [F, E2a, E2b],
    member(F, ['==', '>', '>=', '+', '-', '*', '&&', 'or']),
    subst_(E1a, X, E0, E2a), subst_(E1b, X, E0, E2b).

sameAs(E1, E2) :- normalize(E1, E3), normalize(E2, E3).

normalize(E1, E3) :- rewrite(E1, E2) -> normalize(E2, E3) ; E3 = E1.

rewrite(not(E1a), not(E2a)) :- rewrite(E1a, E2a).
rewrite(E1, E2) :-
    E1 =.. [F, E1a, E1b], E2 =.. [F, E2a, E1b],
    member(F, ['==', '>', '>=', '+', '-', '*', '&&', 'or']),
    rewrite(E1a, E2a).
rewrite(E1, E2) :-
    E1 =.. [F, E1a, E1b], E2 =.. [F, E1a, E2b],
    member(F, ['==', '>', '>=', '+', '-', '*', '&&', 'or']),
    \+ rewrite(E1a, _), rewrite(E1b, E2b).
rewrite(X == X, true).
rewrite(X >= X, true).
rewrite((E1 && E2) && E3, E1 && (E2 && E3)).
rewrite((E1 or E2) or E3, E1 or (E2 or E3)).
rewrite(true && E, E).
rewrite(E && true, E).
rewrite(false or E, E).
rewrite(E or false, E).
rewrite(0 + X, X).
rewrite(X + 0, X).
rewrite(false && _, false).
rewrite(_ && false, false).
rewrite(true or _, true).
rewrite(_ or true, true).
rewrite(0 * _, 0).
rewrite(_ * 0, 0).
rewrite(X >= N1, X > N2) :- integer(N1), N2 is N1 - 1.
rewrite(X >= Y && X > Y, X > Y).
rewrite(X >= Y && not(X > Y), X == Y).
rewrite(N1 >= N2, B) :- integer(N1), integer(N2), N1 > N2 -> B = true; B = false.
rewrite(N1 >= N2, B) :- integer(N1), integer(N2), N1 >= N2 -> B = true; B = false.
rewrite(X - N1 > N2, X > N0) :- integer(N1), integer(N2), N0 is N1 + N2.
rewrite(X > N1 && not(X > N2), X == N2) :- integer(N1), integer(N2), N2 is N1 + 1.
rewrite(X > N1 && X > N2, X > N0) :- integer(N1), integer(N2), N0 is max(N1, N2).
rewrite(X + N1 > N2, X > N0) :- integer(N1), integer(N2), N0 is N2 - N1.
rewrite(X - Y >= 0, X >= Y).
rewrite(X - Y > -1, X >= Y).
rewrite((X + 1) * Y + (Z - Y), X * Y + Z).

implies(E1, E2) :- normalize(E1, E3), normalize(E2, E4), implies_(E3, E4).
implies_(E, E).
implies_(_, true).
implies_(E1 && E2, E3 && E4) :- implies_(E1, E3), implies_(E2, E4).
implies_(E1 && _, E2) :- implies_(E1, E2).
implies_(_ && E1, E2) :- implies_(E1, E2).
implies_(X > N1, X > N2) :- integer(N1), integer(N2), N1 > N2.

test(X) :-
    (X -> R = true; R = fail),
    format('~w ~w.~n', [X, R]),
    R.

prove_skip :- proof({true}; skip(); {true}).
prove_assign :- proof({y == 42}; x = y; {x == 42}).
prove_seq :- proof({x > 4}; (x = x - 1; {x > 3}; x = x - 1); {x > 2}).
prove_if :- proof({true};if(a > b,({true}; r = a),({true}; r = b)); {r == a or r == b}).
prove_while :- proof({x >= 0}; while(x > 0; x = x - 1); {x == 0}).

% x/y qが商でrが余り
sample(
    q = 0;
    r = x;
    while(r >= y;
      r = r - y;
      q = q + 1
    )
).

:- ['SortOfWhile.pro']. % run_div用

run_div :-
  sample(S),
  many(S, [(x, 13), (y, 4)], V),
  member((q, 3), V),
  member((r, 1), V).

prove_div :-
    proof({x >= 0 && y > 0}; % 割り算するときはxが0以上で、yが0より大きいことが必要だ
      ({x >= 0}; % 開始時点ではx >= 0だ
        ( q = 0;
          {x == q * y + x && q >= 0 && x >= 0}; % xはq*y+余り
          ( r = x;
            {x == q * y + r && q >= 0 && r >= 0}; % xはq*y+r
            while(r >= y; ({x == (q + 1) * y + (r - y) && q + 1 >= 0 && r - y >= 0}; % qが1個増えて、rがy減っても成り立つ
                (r = r - y; {x == (q + 1) * y + r && q + 1 >= 0 && r >= 0}; % rを引いたけど問題ないはず
                q = q + 1)
              )
            )
          )
        )
      );
      {x == q * y + r && q >= 0 && r >= 0 && not(r >= y)}). % xはq*y+rでq>=0でr>=0で r < yだと。

main :-
  test(prove_skip),
  test(prove_assign),
  test(prove_seq),
  test(prove_if),
  test(prove_while),
  test(run_div),
  test(prove_div),
  halt.

SortOfWhile.pro

/* Syntax of SortOfWhile */
% Statements

stm(skip()).
stm((S1; S2)) :- stm(S1), stm(S2).
stm(X = E) :- atom(X), aexp(E).
stm(if(E, S1, S2)) :- bexp(E), stm(S1), stm(S2).
stm(while(E; S)) :- bexp(E), stm(S).
stm(or(S1, S2)) :- stm(S1), stm(S2).
stm(par(S1, S2)) :- stm(S1), stm(S2).
stm(abort()).

% Arithmetic expressions

val(X) :- atom(X), X \= true, X \= false.

aexp(N) :- integer(N).
aexp(X) :- val(X).
aexp(E1 + E2) :- aexp(E1), aexp(E2).
aexp(E1 - E2) :- aexp(E1), aexp(E2).
aexp(E1 * E2) :- aexp(E1), aexp(E2).

% Boolean expressions

bexp(true).
bexp(false).
bexp(E1 >= E2) :- aexp(E1), aexp(E2).
bexp(nonzero(E)) :- aexp(E).

/* Big-step */

exec(skip(), M, M).
exec((S1; S2), M1, M3) :- exec(S1, M1, M2), exec(S2, M2, M3).
exec(X = E, M1, M2) :- aeval(E, M1, V), update(M1, X, V, M2).
exec(if(E, S1, _), M1, M2) :- beval(E, M1, true), exec(S1, M1, M2).
exec(if(E, _, S2), M1, M2) :- beval(E, M1, false), exec(S2, M1, M2).
exec(while(E; S), M1, M2) :- beval(E, M1, true), exec((S; while(E; S)), M1, M2).
exec(while(E; _), M, M) :- beval(E, M, false).
exec(or(S1, _), M1, M2) :- exec(S1, M1, M2).
exec(or(_, S2), M1, M2) :- exec(S2, M1, M2).
exec(par(S1, S2), M1, M2) :- exec((S1; S2), M1, M2).
exec(par(S1, S2), M1, M2) :- exec((S2; S1), M1, M2).

aeval(N, _, N) :- integer(N).
aeval(X, M, V) :- atom(X), lookup(M, X, V).
aeval(E1 + E2, M, V3) :- aeval(E1, M, V1), aeval(E2, M, V2), V3 is V1 + V2.
aeval(E1 - E2, M, V3) :- aeval(E1, M, V1), aeval(E2, M, V2), V3 is V1 - V2.
aeval(E1 * E2, M, V3) :- aeval(E1, M, V1), aeval(E2, M, V2), V3 is V1 * V2.

beval(true, _, true).
beval(false, _, false).
beval(E1 >= E2, M, V0) :- aeval(E1, M, V1), aeval(E2, M, V2), (V1 >= V2 -> V0 = true; V0 = false).
beval(nonzero(E), M, V) :- aeval(E, M, 0) -> V = false; V = true.

% Helpers for finite functions as lists of pairs

lookup(L, X, Y) :- append(_, [(X, Y)|_], L).
update(L1, X, Y, L2) :- append(L1a, [(X, _)|L1b], L1) -> append(L1a, [(X, Y)|L1b], L2); L2 = [(X, Y)|L1].



% Testing big-step semantics

:- exec((x=42; x= 88), [], S),S = [(x, 88)].
:- exec((x = 42; while(nonzero(x); x = x - 1)), [], S), S = [(x, 0)].
/* 
:- exec(par(x = 1, (x = 2; x = x + 2)), [], S).
S = [(x, 4)] ;
S = [(x, 1)] ;
false.
*/

/* Small-step */

step((skip(); S), M, S, M).
step((S1; S2), M1, (S3; S2), M2) :- step(S1, M1, S3, M2).
step(X = E, M1, skip(), M2) :- aeval(E, M1, V), update(M1, X, V, M2).
step(if(E, S1, _), M, S1, M) :- beval(E, M, true).
step(if(E, _, S2), M, S2, M) :- beval(E, M, false).
step(while(E; S), M, if(E, (S; while(E; S)), skip()), M).
step(or(S1, _), M, S1, M).
step(or(_, S2), M, S2, M).
step(par(skip(), S), M, S, M).
step(par(S, skip()), M, S, M) .
step(par(S1, S2), M1, par(S3, S2), M2) :- step(S1, M1, S3, M2).
step(par(S1, S2), M1, par(S1, S3), M2) :- step(S2, M1, S3, M2).

final(skip()).

many(S1, M1, M3) :- step(S1, M1, S2, M2), many(S2, M2, M3).
many(S,  M,  M)  :- final(S).

many(S1, M1, S3, M3) :- step(S1, M1, S2, M2), many(S2, M2, S3, M3).
many(S,  M,  S,  M)  :- \+ step(S, M, _, _).

% Testing small-step semantics

:- many((x = 42; x = 88), [], S), S = [ (x, 88)].
:- many((x = 42; while(nonzero(x); x = x - 1)), [], S),
  S = [(x, 0)].
/*
?- many(par(x = 1, (x = 2; x = x + 2)), [], S).
S = [ (x, 4)] ;
S = [ (x, 4)] ;
S = [ (x, 4)] ;
S = [ (x, 4)] ;
S = [ (x, 4)] ;
S = [ (x, 3)] ;
S = [ (x, 3)] ;
S = [ (x, 3)] ;
S = [ (x, 3)] ;
S = [ (x, 3)] ;
S = [ (x, 3)] ;
S = [ (x, 3)] ;
S = [ (x, 1)] ;
S = [ (x, 1)] ;
S = [ (x, 1)] ;
false.

*/