home *** CD-ROM | disk | FTP | other *** search
/ ftp.cs.yorku.ca 2015 / ftp.cs.yorku.ca.tar / ftp.cs.yorku.ca / pub / peter / SVT / SWI / symbex.pl < prev    next >
Text File  |  2007-03-11  |  20KB  |  628 lines
  1. % SYMBOLIC EXECUTION
  2. %   copyright Peter H. Roosen-Runge, 1991-2007
  3.  
  4. % Ver. 2.0, March 5, 1991: handles assignment statements, goals, and IFs. 
  5. %      2.3, Feb. 24, 1992:  Statements can *begin* with an assertion.
  6. %      2.3.1, March 6:  Initial values supplied automatically (again!)
  7. %      3.1 Feb. 27, 1998: uses getTheories to load simplification rules.
  8. %      3.1.2 March 20: clean expressions before converting to term.
  9. %                     allow white space between // and {
  10. %      4.0  Dec. 22, 1998: reads "contracts" and procedure calls
  11. %      4.2.4 March 8: test if assertion is impossible
  12. %      4.2.4.3 March 19: recompiled with clean.prolog v 1.4
  13. %                    allows A[E] in expressions.
  14. %                  still doesn't do parallel assignment
  15. %      4.2.4.6 April 6: print "{", "}" around a statement block
  16. %      4.2.4.8 April 9: repaired procedure post-condition processing
  17. %      4.2.4.9 April 11: simplify if and else conditions before checking
  18. %      4.2.5 March 19, 2000: added multifile and dynamic directives,
  19. %                    processes 'simplification.rules' as a theory file
  20. %                    rather than consulting it. makefun repaired to
  21. %                    allow general pre-conditions as well as identities.
  22. %      4.2.5.1 March 25: checks if simplification.rules exists before
  23. %           trying to open it.
  24.  
  25. %      4.2.6   March 29: symex repaired to handle X or Y conditions
  26. %      5.0     August 25: allow while loops with invariants
  27. %      5.0A    March 31, 2002: attempt to repair from 5.3
  28. %      5.3ASWI February 24, 2007: SWI version
  29. % =====================================================================
  30. % Reads an initial condition in the form
  31. % //{ C and x = e1  and y = e2 . . . etc. } 
  32. % or //{x = e1  and y = e2 . . . and C}
  33. % where the ei are expressions specifying the initial values of variables
  34. % in the code which follows and C is a pre-condition on the initial values.
  35. % The initial condition is followed by a sequence of assignment or 
  36. % IF-statements which are 'symbolically executed'.
  37.  
  38. % a program fragment can be preceded by one more procedure specification 
  39. % in the form
  40. %   //{ precondition }
  41. %   void IDENTIFIER(ARGS);
  42. %   //{ postcondition}
  43.  
  44. % The parameters in the pre- and post-conditions must be in upper case.
  45.  
  46.  
  47. % symbex reports the precondition which holds before THEN or ELSE branches
  48. % and notes branches which are never or always taken.
  49. % Allowable statement forms --
  50. %        V = Expression ;
  51. %        if (B) statement
  52. %        if (B) statement1 else statement2
  53. %               while(B) //{ invariant } statement            
  54. %
  55. %        { statements }
  56.  
  57. % N. B. The right-hand sides of the initial conditions *must not*
  58. % contain occurrences (as atoms) of any variables which occur on the left
  59. % of any equality. You can however use conditions such as x = x(0).
  60.  
  61. % An assertion in the form { proposition } can precede a statement
  62. % or follow the entire code fragment.
  63. % If one occurs, a test is made to see if the previous post-condition
  64. % implies this assertion and the result of the test is reported.
  65. %
  66. % symbex searches the home, working, and working directories for
  67. % arithmetic.simp, equality.simp, and logic.simp, and loads a file 
  68. % "simplification.rules" from the working directory, if there is one.
  69. % 
  70. % ==============================================================
  71.  
  72. % error(Message) :- nl, write('!! '), write(Message), nl, halt.
  73. % user_error_handler(_,_,_,_) :- error('Something wrong.').
  74. %:-unknown(_,fail).
  75. %:- nofileerrors.  (handled in getTheories)
  76.  
  77. :- multifile '->>'/2.  :- dynamic '->>'/2.
  78.  
  79. :- ensure_loaded([qlib(files), qlib(lineio), qlib(ctypes), qlib(occurs) ]).
  80. % qlib(charsio), qlib(lists), qlib(basics) not needed in SWI
  81.  
  82. % For consistency, operator declarations used by wang, taut, simp, symbex, and
  83. % quants.
  84.  
  85. :-op(999,xfx, '!'). % used to separate condition from current function.
  86. :-op(995,xfx, '->>').  % simplification
  87. :-op(995,xfy,'>>').    % sequent
  88. :-op(995,xfy, '::').  % separate parts of a quantified expression
  89. :-op(990, yfx, iff).  % Left-associative (yfx) for consistency with
  90.                       % commutative arithmetic operators.
  91. :-op(1199, xfx, if).  % separate condition from rule.
  92.  
  93. :-op(990,yfx,implies). % for consistency with iff
  94. :-op(980,yfx, [or, cor]).
  95. :-op(970,xfx,xor). % xor isn't associative.  force parenthesization.
  96. :-op(960,yfx,[and, cand, div, mod]).
  97. :-op(950,fy,not).
  98. :-op(700,xfx,assigned).  % used in simplification. A safe 'is' operator.
  99. :-op(700,xfy,['<=','<', '>', '>=', '<>', '==', '!=']).
  100. :-op(200,xfy,'**').
  101. :-op(200,xfy, in).  % used in quants.
  102.  
  103. % uses path in .plrc
  104. :- ensure_loaded([  % lib('input.prolog') for getText(Text)?, loads ctypes
  105.           lib(output), % indent(N), newline, writeString
  106.                   lib(equtaut), lib(simp),
  107.                   lib(clean), % to clean up C 
  108.           lib(charsio), qlib(qlists)]).
  109.  
  110. :-op(100, fx, '&').  % used in symbex for procedure args.
  111.  
  112. % C-operators for symbex and wp.
  113.  
  114. :-op(100, xf,['++', '--']).
  115. :-op(100, fx, ['++', '--']).
  116. :-op(100, xfy, ['+=', '-=', '*=', '/=']).
  117. :-op(601, xfy, ':').
  118. :-op(602, xfy, '?').
  119.  
  120. % =========================================================================
  121.  
  122. activate :- write('Version 5ASWI'), nl,
  123.     getTheories,
  124.         (exists_file('simplification.rules'),
  125.                theory('simplification.rules'); true),
  126.     readCode(C), !, program(C), 
  127.         nl, halt.
  128. %     ;
  129. %    error('Something wrong.').
  130.  
  131. % read lines of code and concatenate into Code.
  132. readCode(Code) :-
  133.         get_line(Line, Terminator),
  134.        (
  135.         is_endfile(Terminator), Code = Line
  136.         ;
  137.         readCode(More), append(Line,More, Code)
  138.        ).   
  139.  
  140. testInput2("if(b) x = y+2; if(!b) x = y + 2; x=y;").
  141. testInput3("//{ true } void swap(X, Y); //{ X = 'old Y' and Y = 'old X'}
  142. x=7; swap(&x, &y);").
  143. testInput4("//{x=a and y=0 and a > 0}
  144. while(x != 0) //{x+y=a}{ x = x-1; y = y+1;}").
  145.  
  146. program(S0) :- 
  147.     fixComment(S, S0, []),
  148.     contracts(S, S1),
  149.     precond0(P,S1,S2), 
  150.     makefun(P, C, F), !,  % C is true by default
  151.     applyFun(F, C, CC),
  152.     statement(1, CC ! F, NewF, S2, Rest), !,
  153.     statements(1, NewF, Post, Rest, LeftOver), 
  154.     unfun(Post, PostTerm),
  155.     simplify(PostTerm, SimpPost),
  156.     nl, writeCond(SimpPost),
  157.     testContra(SimpPost),
  158.     break(LeftOver, Remains),
  159.         (Remains == [] 
  160.     ;
  161.          nl, writeStrings(["// Couldn't parse: ", Remains])
  162.     ).
  163.  
  164. contracts --> break, contract, (contracts ; []) ; [].
  165.  
  166. opT([OpC | "="], OpT) :- atom_codes(OpT, [OpC]).
  167.     
  168. precond0(P) --> break, precond(P), break.
  169. precond(true) -->  "//", break, [12, 12], break, { nl, writeCond(true) }. 
  170. precond(PTerm) --> "//", break, [12], upto(P, [12]), break,
  171.         {  chars_to_term(P, PTerm)
  172. %    ,   nl, writeCond(PTerm) 
  173.         }.
  174. precond(true) --> break, { nl, writeCond(true) }.
  175.  
  176. goal(N, Cond) --> "//", break, [12], upto(Goal, [12], [12]), !, 
  177.     { 
  178.       chars_to_term(Goal, GoalTerm), unfun(Cond, CTerm),
  179.       simplify(GoalTerm, SimGoal),
  180.       indent(N), write('// assert: '), write(SimGoal),
  181.       (
  182.         simtaut(not(CTerm and SimGoal)),
  183.             indent(N), write('// -- assertion is impossible!'),
  184.         indent(N), write('// -- current state is '),
  185. %           pretty(CTerm)
  186.                write(CTerm), nl
  187.            ;  
  188.        simtaut(CTerm implies SimGoal), 
  189.         indent(N), write('// -- assertion is verified.'), nl
  190.            ;
  191.         indent(N), write('//  -- assertion may not be valid.'),
  192.         indent(N), write('//  -- could not prove '),
  193. %            pretty(CTerm implies SimGoal)
  194.                 write(CTerm implies SimGoal), nl
  195.       )
  196.      }, break.
  197.  
  198. unfun(P ! [], P).    
  199. unfun(P ! F, SPT) :- unfun1(F, Term), simplify(P and Term, SPT).
  200. unfun(Rest or P, SYX) :- unfun(P, Y), unfun(Rest, X), simplify(X or Y, SYX).
  201. unfun(_, _) :- error('Error in unfun.').
  202.  
  203. unfun1([[R, V]], R=V).
  204. unfun1([[R, V] | Rest], Term and (R=V)) :- unfun1(Rest, Term).
  205. unfun1(_, _) :- error('Error in unfun.').
  206.  
  207. /*
  208. processAssign(X=V, Args, In, Pin, Pin,  Out) :-
  209.         memberchk(&X, Args),
  210.         symex(In, X, V, Out).
  211. processAssign(Rest and (X=V), Args, In, Pin, Pin, Out) :-
  212.         memberchk(&X, Args),
  213.         symex(In, X, V, Out1),
  214.         processAssign(Rest, Args, Out1, Pin, Pin, Out).
  215. processAssign(T, _, In, Pin, Pin and T, In).
  216. */
  217.  
  218. assignDummy(X, Args, In, V, Out, InList, [DummyX | InList]) :-
  219.         memberchk(&X, Args),
  220.         name(X,XStr), name('$', [Dollar]), name(DummyX, [Dollar|XStr]),
  221.         symex(In, DummyX, V, Out).
  222.  
  223. processAssign1(X=V, Args, In, Pin, Pin,  Out, InList, OutList) :-
  224.         assignDummy(X, Args, In, V, Out, InList, OutList).
  225.  
  226. processAssign1(Rest and (X=V), Args, In, Pin, Pin, Out, InList, OutList) :-
  227.         assignDummy(X, Args, In, V, Out1, InList, NewList),
  228.         processAssign1(Rest, Args, Out1, Pin, Pin, Out, NewList, OutList).
  229.  
  230. unassignDummy(X, In, Out) :-
  231.         name('$', [Dollar]), name(X, [Dollar|XStr]), name(UnDollar, XStr),
  232.         symex(In, UnDollar, X, Out).
  233. processAssign1(T, _, In, Pin, Pin and T, In).
  234.  
  235. deleteDollar([], In, In).
  236. deleteDollar([[X, _] | Rest], In, Out) :-
  237.         name('$', [Dollar]), name(X, [Dollar|_]),
  238.         deleteDollar(Rest, In, Out).
  239. deleteDollar([[X, Y] | Rest], In, Out) :-
  240.         deleteDollar(Rest, [[X, Y] | In], Out).
  241.  
  242. processAssign2([], P ! In, P ! Cleaned) :- deleteDollar(In, [], Cleaned).
  243. processAssign2([X | List], In, Out) :-
  244.         unassignDummy(X, In, New),
  245.         processAssign2(List, New, Out).
  246.  
  247. processAssign(T, Args, In, Pin, Pout, Out) :-
  248.         processAssign1(T, Args, In, Pin, Pout, New, [], OutList),
  249.         processAssign2(OutList, New, Out).
  250.  
  251. processPostCon(Rest and T, In, Out) :-
  252.        combine(In, T, Out1),
  253.        processPostCon(Rest, Out1, Out).   
  254. processPostCon(P, In, Out) :-
  255.        combine(In, P, Out).
  256.  
  257. processPostCon(P, Args, In, Out) :-
  258.     processAssign(P, Args, In, true, Pout, Out1),
  259.     processPostCon(Pout, Out1, Out).
  260.  
  261. statements(N, Pre, Post)  --> 
  262.     statement(N, Pre, PP), 
  263.     statements(N, PP, Post).
  264. statements(_, Pre, Pre) --> [].
  265.  
  266. statement(N, Pre, Pre) --> goal(N, Pre), break.
  267. statement(N, Pre, Pre) --> 
  268.     ";", break,
  269.     {indent(N), write(';')}.
  270. statement(N, Pre, Post) --> 
  271.     matchP("{", "}", Balanced),
  272.     { 
  273.       indent(N), write('{ '),
  274.           statements(N, Pre, Post, Balanced, []),
  275.           indent(N), write(' }')
  276.     }, 
  277.     break.
  278.  
  279. statement(N, Pre, IfPost or ElsePost) -->
  280.                 ifThen(N, Pre, BTerm, IfPre), break,
  281.                 statement(N+1, IfPre, IfPost), break,
  282.                 elseClause(N, Pre, BTerm, ElsePost), break.
  283.  
  284. statement(N, Pre, Post) -->
  285.         "while", break, matchP("(", ")", B), break, !,
  286.         { indent(N), writeStrings(["while (", B, ") "]),
  287.           string_to_term(B, BTerm),
  288.           combine(Pre, BTerm, Entry) },
  289.         assertion(Inv), 
  290.        {string_to_term(Inv, InvTerm), 
  291.         unfun(Entry, EntryP),
  292.         (
  293.          simtaut(EntryP implies InvTerm)
  294.         ;
  295.          indent(N+1), 
  296.      write('Cannot prove that the invariant holds at loop entry.')
  297.         )
  298.        },
  299.     statement(N+1, Entry, Exit),
  300.        {unfun(Exit, ExitP),
  301.         (simtaut(ExitP implies InvTerm)
  302.         ;
  303.          indent(N+1),
  304.          write('Cannot prove that the invariant holds at loop exit.')
  305.         ),
  306.         combine(Pre, InvTerm and not BTerm, Post)
  307.        }.
  308.                     
  309. statement(N, Cond, NewCond) -->
  310.      "switch", break, matchP("(", ")", Var), break,
  311.     {indent(N), writeStrings(["switch (", Var, ") {"])},
  312.      matchP("{", "}", Cases), break,
  313.     { cases(N, Cond, NewCond, Var, Cases, [])}, break.
  314.  
  315. statement(N, Cond, NewCond) -->
  316.          opAssign(Ref, Val, OpAssign),
  317.         { 
  318.      opT(OpAssign, OpT),   
  319.      atom_codes(OpT, OpString),
  320.      indent(N),
  321.      writeStrings([Ref, " = ", Ref, OpString, Val, " ;"]),
  322.          chars_to_term(Ref, R), string_to_term(Val, V),
  323.          RHS =.. [OpT, R, V],  
  324.          symex(Cond, R, RHS, NewCond), !
  325.     }, 
  326.     break.
  327. statement(N, Cond, NewCond) -->
  328.         upto(Ref, "=", ";"), upto(Val, ";"),
  329.         { 
  330.      indent(N), writeStrings([Ref, " = ", Val, " ;"]),
  331.          chars_to_term(Ref, R), string_to_term(Val, V),
  332.          symex(Cond, R, V, NewCond), !
  333.     }, 
  334.     break.            
  335. statement(N, Cond, NewCond) -->
  336.     incdec(Ref, Op), break,
  337.     { 
  338.           indent(N), writeStrings([Ref, " = ", Ref, " ", [Op], " 1;"]),
  339.           chars_to_term(Ref, R), atom_chars(OpT, [Op]),
  340.       RHS =.. [OpT, R, 1],
  341.       symex(Cond, R, RHS, NewCond), !
  342.          }.
  343. statement(N, Pre, Post) -->
  344.     upto(Call,  ";", ";"), break,
  345.     { doCall(N, Pre, Call, Post), !}.
  346.  
  347.  
  348. cases(N, PreCases, PostCases, V) -->
  349.     "case ", break, upto(Case, ":", ":"), break,
  350.     {
  351.          indent(N+1), writeStrings(["case: ", Case]),
  352.          append([V," == ", Case], B),
  353.          string_to_term(B, BTerm),
  354.          combine(PreCases, BTerm, PreCase), unfun(PreCase, UPreCase),
  355.      writeCond(UPreCase)
  356.      },
  357.      caseStatements(N+1, PreCase, PostCase), break,
  358.      cases(N, PreCases, PostCases, V)
  359.        ;
  360.         "default ", break, ":", break, 
  361.     { 
  362.       indent(N+1), write('default :'),
  363.       unfun(PreCases, UPreCases),
  364.          writeCond(UPreCases) 
  365.     },
  366.     statements(N+1, PreCases, PostCases), 
  367.     ("break ", break, ";" , break ; break) % last break optional
  368.        ;
  369.        break.  % default optional.
  370.  
  371. caseStatements(N, PreCase, PostCase) -->
  372.     "break ", break, ";", break
  373.        ;
  374.         "case ", break, ":", break, caseStatements(N, PreCase, PostCase)
  375.        ;
  376.         statement(N, PreCases, PostCases),
  377.     caseStatements(N,  PreCase, PostCase)
  378.        ;
  379.         break.
  380.                                           
  381. incdec(Ref, Op) -->
  382.      {memberchk(OpC, ["++", "--"])},
  383.      upto(Ref, OpC, ";"), break, ";", break,
  384.      {OpC = [Op, Op]}.
  385.          
  386. doCall(N, Pre, Call, Post) :-
  387.      indent(N), writeStrings([Call, ";"]),
  388.      chars_to_term(Call, CallTerm),
  389.          contract(PreCon1, CallTerm, PostCon1), !,
  390.      cleanPointers(PreCon1, PreCon), cleanPointers(PostCon1, PostCon),
  391.      unfun(Pre, PreProp),
  392.      simplify(PreProp implies PreCon, SimpCon), 
  393.      ( 
  394.       tautology(SimpCon)
  395.      ; 
  396.       indent(N), write( '... cannot show '), 
  397. %      pretty(SimpCon), 
  398.           write(SimpCon),
  399.       write(' for '),
  400.       write(CallTerm), write('.')
  401.      ),
  402.       CallTerm =.. [_ | Args],
  403.       processPostCon(PostCon, Args, Pre, Post).
  404.  
  405. elseClause(N, Pre, BTerm, Post) --> 
  406.     "else", break,
  407.     { indent(N), write('else '),
  408.       combine(Pre, not BTerm, EP), unfun(EP, UEP),
  409.       simplify(UEP, SUEP), writeCond(SUEP),
  410.       checkCond(N, Pre, SUEP),
  411.       !},
  412.     statement(N+1, EP, Post).
  413. elseClause(_, Pre, BTerm, Post) --> 
  414.     { combine(Pre, not BTerm, Post), !}.
  415.  
  416. ifThen(Indent, Pre, BTerm, IfP) --> 
  417.     "if", break, matchP("(", ")", B), break,
  418.         { indent(Indent), writeStrings(["if (", B, ") "]),
  419.       string_to_term(B, BTerm),
  420.           combine(Pre, BTerm,IfP), unfun(IfP, UIfP),
  421.       simplify(UIfP, SUIfP), writeCond(SUIfP),
  422.       checkCond(Indent, Pre, SUIfP),
  423.       ! }.
  424.  
  425. opAssign(Ref, Val, OpAssign) -->
  426.     { member(OpAssign, ["+=", "*=", "/=", "&=", "-=", "|="])},
  427.         upto(Ref, OpAssign, ";"),  upto(Val, ";", ";").
  428.  
  429. checkCond(Indent, Pre, C) :- unfun(Pre, UPre), 
  430.      ( simtaut(UPre implies C) ->
  431.     indent(Indent), write('// This branch is always taken.')
  432.      ;
  433.        simtaut(UPre implies not C) ->  
  434.         indent(Indent), write('// This branch is never taken.')
  435.      ;
  436.       true
  437.      ).
  438.  
  439. pretty(P) :- pretty(P, 72).
  440.  
  441. writeCond(P) :- write('//{ '), writeC(P), write(' }').
  442. % writeC(P ! []) :- pretty(P).
  443. writeC(P ! []) :- write(P).
  444. % writeC(P ! F) :- pretty(P), write(' and '), writeF(F).
  445. writeC(P ! F) :- write(P), write(' and '), writeF(F).
  446. writeC((P ! F) or Rest) :- 
  447.     write('( '), writeC(P ! F), write(' )'), write(' or '), writeC(Rest).
  448. % writeC(P) :- pretty(P).
  449. writeC(P) :- write(P).
  450.  
  451. combine(P ! F, B, S ! F) :- 
  452.     applyFun(F, B, Result), simplify(P and Result, S).
  453. combine(Rest or (P ! F), B, RestP or S) :-
  454.     combine(P ! F, B, S),
  455.     combine(Rest, B, RestP).
  456. combine(_,_,_) :- error('!! Error in combine procedure.').
  457.  
  458.  
  459. symex(P ! F, R, V, NewCond) :-
  460.           \+ member([R, _], F),
  461.          applyInitial1(R, V, ModifiedV),
  462.          applyInitial1(R, P, ModifiedP),
  463.          applyInitial(R, F, ModifiedF),
  464.          symex0(ModifiedP ! ModifiedF, R, ModifiedV, NewCond)
  465.      ; 
  466.              symex0(P ! F, R, V, NewCond).
  467.  
  468. symex(X, R, V, N) :-
  469.         symex0(X, R, V, N)
  470.     ;
  471.         error('Bug in symex.').
  472.         
  473. symex0(P ! F, R, V, NewP ! NewF) :- symex1(P ! F, R, V, NewP ! NewF).
  474. symex0(Rest or (P ! F), R, V, Result or (NewP ! NewF)) :-
  475.         symex(P ! F, R, V, NewP ! NewF), symex(Rest, R, V, Result).
  476. symex0(Branch1 or Branch2, R, V, Result1 or Result2) :-
  477.     symex(Branch1, R, V, Result1), symex(Branch2, R, V, Result2).
  478. symex1(P ! F, R, V, NewP ! NewF) :-
  479.         applyFun(F, V, NewV),
  480.         simplify(NewV, SimV),
  481.         update(F, R, SimV, NewF),
  482.         applyFun(NewF, P, NewP).
  483.  
  484. applyInitial1(V, Expr, Result) :-
  485.         path_arg(Path, Expr, V), makeOld(V, OldV),
  486.         change_path_arg(Path, Expr, Modified, OldV),
  487.         !,
  488.         applyInitial1(V, Modified, Result).
  489. applyInitial1(_, Expr, Expr).   
  490.  
  491. makeOld(V, OldV) :-
  492.         atom_codes(V, Vstr), 
  493.        (
  494.         append("old", _, Vstr), OldV = V
  495.        ;
  496.     append("old ", Vstr, OldVstr),
  497.         atom_codes(OldV, OldVstr)
  498.        ).
  499.  
  500.  
  501. applyInitial(_, [], []).
  502. applyInitial(Initial, [[Z, Expr] | Rest], [[Z, Applied] | AppliedRest]) :-
  503.         applyInitial1(Initial, Expr, Applied),
  504.         applyInitial(Initial, Rest, AppliedRest).
  505.  
  506.  
  507. % based on Quintus Prolog Library Manual, p. 40
  508. applyFun(Function, Expr, Final) :-
  509.         path_arg(Path, Expr, Lhs), 
  510.     (
  511.      Lhs = 'OLD'(A), 
  512.      ( memberchk([A, E], Function) -> Rhs = E
  513.       ;
  514.        makeOld(A, Rhs)
  515.          )
  516.     ;
  517.      atom(Lhs), memberchk([Lhs, Rhs], Function)
  518.     ),
  519.         change_path_arg(Path, Expr, Modified, Rhs),
  520.         !,
  521.         applyFun(Function, Modified, Final).
  522. applyFun( _, Expr, Expr).
  523.  
  524. update(F, R, NewV, NewF) :-
  525.     change_path_arg(_, F, [R, _], NewF, [R, NewV])
  526.     ;
  527.     append([[R, NewV]], F, NewF).
  528.  
  529. writefun([]).
  530. writefun(F) :- write('{ '), writeF(F), write(' }').
  531. writeF([[R,V] | Rest]) :-  write(R = V), writeF1(Rest).
  532. writeF1([]).
  533. writeF1([[R, V] | Rest]) :- write(' and '), write(R = V), writeF1(Rest).
  534. /*
  535. makefun(X=Y, C, [[X,Y]]) :- 
  536.     atom(X), 
  537.     (
  538.      free_of_term(X,Y), 
  539.      (var(C) -> C = true ; true)
  540.     ; 
  541.      error('Something wrong in the initial condition.')
  542.     ).
  543. makefun(Rest and X=Y, C, [[X,Y] | RestF]) :- atom(X), makefun(Rest, C, RestF).
  544. makefun(F and C, C, FList) :- makefun(F, C, FList).
  545. makefun(C, C, []) :- var(C) -> C=true ; true.
  546. makefun(_,_,_) :- error('Something wrong in the initial condition.').
  547. */
  548. % makefun(InCon, OutCon, Flist)
  549. makefun(C, C, []) :- var(C) -> C=true.
  550. makefun(X=Y, C, [[X,Y]]) :-
  551.         atom(X),
  552.         (
  553.          free_of_term(X,Y),
  554.          (var(C) -> C = true ; true)
  555.         ).
  556.  
  557. makefun(Rest and X=Y, C, [[X,Y] | RestF]) :- atom(X), makefun(Rest, C, RestF).
  558. makefun(F and C,NewC and C, FList) :- makefun(F, NewC, FList).
  559. makefun(C, C, []).
  560. makefun(_,_,_) :- error('Something wrong in the initial condition.').    
  561.  
  562. contract -->
  563.     assertion(Pre),
  564.     proc(Call),
  565.     assertion(Post),
  566.       { nl, nl,
  567.         append(["contract(", Pre, ",",  Call, ",", Post, ")"], ContractString),
  568.     mapOld(ContractString, Contract),
  569.     chars_to_term(Contract, ContractTerm),
  570.     assertz(ContractTerm)
  571.        }.
  572.  
  573. mapOld(Old, New) :-
  574.         mapOld1(Prefix, NewSubstring, Old, Rest),
  575.         mapOld(Rest, NewRest),
  576.         append([Prefix, NewSubstring, NewRest], New).
  577. mapOld(Old, Old).
  578.  
  579.  
  580. mapOld1(Prefix, New) --> 
  581.     upto(Prefix, "'","'"),
  582.     "old ", upto(Var, "'", "'"),
  583.     {append(["'OLD'(", Var, ")"], New)}.
  584.  
  585. unmapOld(Term, New) :-
  586.     path_arg(Path, Term, 'OLD'(X)),
  587.     atom_codes(X, Name),
  588.     append("old ", Name, OldName),
  589.     atom_chars(Atom, OldName),
  590.         change_path_arg(Path, Term, Modified, Atom),
  591.         !,
  592.         unmapOld(Modified, New).   
  593. unmapOld(Term, Term).
  594.  
  595. assertion(P) --> "//", break, [12], upto(P, [12], ";"), break,
  596.     {nl, writeStrings(["//{ ", P, " }"]), !}.
  597.  
  598. proc(Call) -->
  599.     "void ", upto(Call, ";", ";"), break,
  600.     {nl, writeStrings(["void ", Call, ";"]), !}.
  601.  
  602. cleanPointers(Expr, Final) :-
  603.         path_arg(Path, Expr, &X),
  604.         change_path_arg(Path, Expr, Modified, X),
  605.         !,
  606.         cleanPointers(Modified, Final).
  607. cleanPointers(Expr, Expr).                 
  608.  
  609. testContra(Prop) :-
  610.     simtaut(not(Prop)) ->
  611.       nl, write('The final state is a contradiction.'), nl
  612.        ;
  613.         true.
  614.  
  615. simtaut(T) :- simplify(T, ST), !, tautology(ST).
  616.  
  617.  
  618.  
  619.  
  620.  
  621.  
  622.  
  623.  
  624.  
  625.  
  626.  
  627.  
  628.