:- encoding(utf8). % Verification Generator for Simple Imperative Programs % % by Bharat Jayaraman (VC Generation) % State Univ of New York at Buffalo % and % M.K. Jinesh (Web Interface) % Amrita University :- op(550, xfx, '@'). :- op(550, xfx, '%'). :- op(650, xfy, '::'). :- op(650, xfx, '~>'). :- op(600, yfx, '&&'). :- op(620, yfx, '||'). :- op(650, xfx, '<=>'). :- op(650, xfx, '==>'). :- op(650, xfx, '=<'). :- op(650, xfx, '>='). :- op(650, xfx, '!='). :- op(650, xfx, '=='). :- op(650, xfx, '>'). :- op(650, xfx, '<'). :- dynamic array_type/2. :- dynamic logic_vars/1. :- dynamic context/1. :- dynamic vc_count/2. :- dynamic contracted_function/6. :- dynamic call_result_counter/1. :- discontiguous verify/1, verify_data/1. % Web Interface :- use_module(library(http/thread_httpd)). :- use_module(library(http/http_dispatch)). :- use_module(library(http/http_header)). :- use_module(library(http/http_multipart_plugin)). :- use_module(library(http/http_client)). :- use_module(library(http/html_write)). :- use_module(library(option)). :- use_module(library(http/http_parameters)). :- use_module(library(memfile)). :- use_module(library(http/http_json)). :- use_module(library(filesex)). % delete_file/1 % :- use-module(library(apply)). :- use_module(library(error)). % must_be/2 :- public save_file/3. :- http_handler(root(.), get_gui, []). :- http_handler(root(upload), upload, []). :- http_handler(root(verify), call_verify, []). :- http_handler(root(altergo), call_alt_ergo, [method(post)]). % swipl -O --goal=start_server --stand_alone=true -o vcgen -c vcgen.pl % ===================================================================== % ---- Config alt_ergo_path(Path) :- current_prolog_flag(argv, Args), ( member(Argument, Args), atom_concat('--alt-ergo=', Path, Argument) -> true ; Path = path('alt-ergo') ). % An OPAM-installed Alt-Ergo on Windows needs both its executable directory % and OPAM's MinGW runtime directory on PATH. A GUI-launched SWI-Prolog does % not inherit the environment produced by "opam env", so add them here. alt_ergo_process(Command, []) :- current_prolog_flag(windows, true), !, ensure_windows_alt_ergo_path, alt_ergo_path(Command). alt_ergo_process(Command, []) :- alt_ergo_path(Command). ensure_windows_alt_ergo_path :- getenv('LOCALAPPDATA', LocalAppData), directory_file_path(LocalAppData, opam, OpamRoot), directory_file_path(OpamRoot, default, DefaultSwitch), directory_file_path(DefaultSwitch, bin, AltErgoBin), directory_file_path(OpamRoot, '.cygwin', Cygwin), directory_file_path(Cygwin, root, CygwinRoot), directory_file_path(CygwinRoot, usr, Usr), directory_file_path(Usr, 'x86_64-w64-mingw32', MingwTarget), directory_file_path(MingwTarget, 'sys-root', SysRoot), directory_file_path(SysRoot, mingw, Mingw), directory_file_path(Mingw, bin, RuntimeBin), getenv('PATH', OldPath), atomic_list_concat([AltErgoBin, RuntimeBin, OldPath], ';', NewPath), setenv('PATH', NewPath). alt_ergo_time_limit_sec(1). % hard cap per request, adjust as needed % server(Port) :- http_server(http_dispatch, [port(Port)]). % ---------- Request handler (always replies JSON) ---------- call_alt_ergo(Request) :- catch(call_alt_ergo_unsafe(Request, Reply), E, ( message_to_string(E, Msg), Reply = _{status:"error", raw:Msg})), reply_json_dict(Reply, [status(200)]). call_alt_ergo_unsafe(Request, _{status:Status, raw:PrettyAtom}) :- % Read body as JSON or plain text ( memberchk(content_type(CT), Request), sub_atom(CT, 0, _, _, 'application/json') -> http_read_json_dict(Request, D), VCText = D.vcText ; memberchk(input(In), Request), memberchk(content_length(Len), Request), set_stream(In, buffer(full)), read_string(In, Len, VCText) ), % Run Alt-Ergo with hard timeout alt_ergo_time_limit_sec(Limit), run_alt_ergo_file_ae_with_timeout(VCText, Limit, Exit, TimedOut, Stdout, Stderr), % Alt-Ergo on Windows may write a harmless timelimit warning to stderr % while writing the actual proof results to stdout. Prefer proof output. ( Stdout \= "" -> Raw0 = Stdout ; Raw0 = Stderr ), % Produce pretty 1-line-per-goal summary (robust) pretty_alt_ergo_safe(Raw0, TimedOut, VCText, PrettyText), append_prover_diagnostics(PrettyText, Exit, Stderr, PrettyWithDiagnostics), atom_string(PrettyAtom, PrettyWithDiagnostics), % Status for UI ( TimedOut == true -> Status = "error" ; Exit = exit(0) -> Status = "ok" ; Status = "error" ). append_prover_diagnostics(Pretty,exit(0),_,Pretty) :- !. append_prover_diagnostics(Pretty,_,"",Pretty) :- !. append_prover_diagnostics(Pretty,_,Stderr,WithDiagnostics) :- sanitize_string(Stderr,CleanError), format(string(WithDiagnostics), "~w~n~nProver diagnostics:~n~w", [Pretty,CleanError]). % ---------- Alt-Ergo runner with timeout ---------- run_alt_ergo_file_ae_with_timeout(VCText, LimitSec, Exit, TimedOut, Stdout, Stderr) :- must_be(integer, LimitSec), tmp_file(alt_ergo, Base), file_name_extension(Base, ae, Path), setup_call_cleanup( open(Path, write, S, [encoding(utf8)]), format(S, "~s", [VCText]), close(S)), alt_ergo_process(Command, PrefixArgs), % CLI caps: return quickly (mimic online behavior) append(PrefixArgs, ['--timelimit=1', '--steps-bound=2000', Path], AEArgs), setup_call_cleanup( ( process_create(Command, AEArgs, [ stdout(pipe(Out)), stderr(pipe(Err)), process(PID) ]), retractall(ae_timeout_flag(_)), asserta(ae_timeout_flag(false) ), alarm(LimitSec, ae_kill_on_timeout(PID, Out, Err), AlarmID) ), ( read_string(Out, _, Stdout), read_string(Err, _, Stderr), process_wait(PID, Exit) ), ( remove_alarm(AlarmID), ( catch(close(Out), _, true), catch(close(Err), _, true) ) ) ), catch(delete_file(Path), _, true), (ae_timeout_flag(true) -> TimedOut = true ; TimedOut = false ). :- thread_local ae_timeout_flag/1. ae_kill_on_timeout(PID, Out, Err) :- retractall(ae_timeout_flag(_)), asserta(ae_timeout_flag(true)), catch(process_send_signal(PID, term), _, true), sleep(0.2), catch(process_send_signal(PID, kill), _, true), % The request handler owns these streams. Closing them from the alarm % callback races with read_string/3 and caused "stream does not exist". ignore(Out = Out), ignore(Err = Err). % ---------- Robust pretty-printer (never throws) ---------- pretty_alt_ergo_safe(Raw, TimedOut, VCText, PrettyText) :- sanitize_string(Raw, Clean), split_string(Clean, "\n", "\r", Lines0), include(is_result_line_or_unknown, Lines0, Hits0), % Strip "File /tmp/..." prefixes before parsing maplist(strip_file_prefix, Hits0, Hits1), maplist(format_result_line_ci(TimedOut), Hits1, PrettyLines0), % Alt-Ergo may return only the goals it proved before a timeout or an % inconclusive search. Reconcile its response with every generated goal % so failed/missing goals never disappear from the UI. goals_from_input(VCText, GoalNames), reported_goals(Hits1, ReportedGoals), missing_goals(GoalNames, ReportedGoals, MissingGoals), maplist(as_unknown_line, MissingGoals, MissingLines), append(PrettyLines0, MissingLines, PrettyLines), ( PrettyLines \= [] -> atomic_list_concat(PrettyLines, '\n', PrettyText) ; GoalNames = [] -> normalize_space(string(PrettyText), Clean) ). reported_goals([],[]). reported_goals([Line|Lines],Goals) :- ( extract_goal_name(Line,Goal) -> Goals=[Goal|Rest] ; Goals=Rest ), reported_goals(Lines,Rest). missing_goals([],_,[]). missing_goals([Goal|Goals],Reported,Missing) :- ( memberchk(Goal,Reported) -> Missing=Rest ; Missing=[Goal|Rest] ), missing_goals(Goals,Reported,Rest). sanitize_string(In, Out) :- % remove ASCII control chars except tab/newline split_string(In, "", "\u0000\u0001\u0002\u0003\u0004\u0005\u0006\u0007\u0008\u000B\u000C\u000E\u000F\u0010\u0011\u0012\u0013\u0014\u0015\u0016\u0017\u0018\u0019\u001A\u001B\u001C\u001D\u001E\u001F", [Out]). contains_ci(Str, Needle) :- string_lower(Str, SL), string_lower(Needle, NL), sub_string(SL, _, _, _, NL). is_result_line_or_unknown(Line) :- contains_ci(Line, "goal"), ( contains_ci(Line, "valid") ; contains_ci(Line, "qed") ; contains_ci(Line, "invalid") ; contains_ci(Line, "unknown") ; contains_ci(Line, "i don't know") ; contains_ci(Line, "cannot decide") ). % Remove "File ...: " prefix if present strip_file_prefix(Line, Clean) :- ( sub_string(Line, _, _, _, ": Valid") ; sub_string(Line, _, _, _, ": Invalid") ; sub_string(Line, _, _, _, ": Unknown") ; sub_string(Line, _, _, _, ": Qed") ), sub_atom(Line, After, _, _, ":"), Start is After + 1, sub_string(Line, Start, _, 0, Rest), normalize_space(string(Clean), Rest), !. strip_file_prefix(Line, Clean) :- normalize_space(string(Clean), Line). format_result_line_ci(_, Line, Out) :- ( contains_ci(Line, "valid") -> Status = "Valid" ; contains_ci(Line, "qed") -> Status = "Valid" ; contains_ci(Line, "invalid") -> Status = "Invalid" ; contains_ci(Line, "unknown") -> Status = "Unknown" ; Status = "Unknown" ), extract_goal_ci(Line, Goal0), ( Goal0 = "" -> Goal = "unknown" ; Goal = Goal0 ), extract_time_ci(Line, Time), extract_steps_ci(Line, Steps), %( TimedOut == true, Status \= "Valid", Status \= "Invalid" %-> Sfx = " (timeout)" ; Sfx = ""), ( Time = "" -> TPart = "" ; format(string(TPart), "~w", [Time]) ), ( Steps = "" -> SPart = "" ; format(string(SPart), " (~w steps)", [Steps]) ), status_emoji(Status, Emoji), format(string(Out), "~w ~w: ~w ~w ~w", [Emoji, Goal, Status, TPart, SPart]). status_emoji("Valid", " ✅ "). status_emoji("Unknown", " ⚠️ "). status_emoji("Invalid", " ❌ "). extract_goal_ci(Line, Goal) :- extract_goal_name(Line, Goal). extract_time_ci(Line, Time) :- findall(InnerClean, ( sub_string(Line, A, _, _, "("), sub_string(Line, A, L, _, ")"), sub_string(Line, A, L, _, Seg), sub_string(Seg, 1, _, 1, Inner), normalize_space(string(InnerClean), Inner), ( contains_ci(InnerClean, "ms") ; contains_ci(InnerClean, "s") )), Ts), ( Ts = [Time|_] -> true ; Time = "" ). extract_steps_ci(Line, Steps) :- ( contains_ci(Line, " steps)"), sub_string(Line, Open, _, _, "("), sub_string(Line, Close, _, _, " steps)"), Open < Close, Start is Open+1, Len is Close-Start, sub_string(Line, Start, Len, _, Inside), normalize_space(string(Steps0), Inside), Steps = Steps0 -> true ; Steps = "" ). as_unknown_line(Goal, Line) :- format(string(Line), " ⚠️ ~w: Unknown (no prover result)", [Goal]). goals_from_input(VCText, Names) :- split_string(VCText, "\n", "\r", Lines), include(looks_like_goal_decl, Lines, GoalLines0), % NEW: strip any "File ..." prefix in VC lines before extracting names maplist(strip_file_prefix, GoalLines0, GoalLines), maplist(extract_goal_name_from_decl, GoalLines, Names0), exclude(=( ""), Names0, Names). looks_like_goal_decl(Line) :- contains_ci(Line, "goal"). extract_goal_name_from_decl(Line, Name) :- ( extract_goal_name(Line, Name0) -> Name = Name0 ; Name = "" ). % Read the whole identifier following "goal", stopping at whitespace or % the punctuation used in declarations and Alt-Ergo result lines. extract_goal_name(Line, Name) :- string_lower(Line, Lower), sub_string(Lower, GoalPos, 4, _, "goal"), AfterGoal is GoalPos + 4, sub_string(Line, AfterGoal, _, 0, Rest), split_string(Rest, " \t\r\n:;()", " \t\r\n:;()", [Name|_]), Name \= "". % ====================================================================== start_server :- server(8080). server(Port) :- http_server(http_dispatch, [port(Port)]). get_gui(_Request) :- get_template(X), format('Content-type: text/html; charset=UTF-8~n~n'), format(X, [' ',' ']). upload(Request) :- multipart_post_request(Request), !, http_read_data(Request, [file=Data], []), get_template(X), format('Content-type: text/html; charset=UTF-8~n~n'), format(X, [Data,' ']). upload(_Request) :- throw(http_reply(bad_request(bad_file_upload))). call_verify(Request) :- member(method(post), Request), !, http_read_data(Request, [content=Data],[]), tmp_file('txt',Name), tell(Name), verify_data(Data), told, open(Name,read,Stream1), read_string(Stream1,_,Output), close(Stream1), get_template(X), format('Content-type: text/html; charset=UTF-8~n~n'), format(X, [Data,Output]). multipart_post_request(Request) :- memberchk(method(post), Request), memberchk(content_type(ContentType), Request), http_parse_header_value( content_type, ContentType, media(multipart/'form-data', _)). save_file(In, file(FileName, File), Options) :- option(filename(FileName), Options), setup_call_cleanup( tmp_file_stream(octet, File, Out), copy_stream_data(In, Out), close(Out)). get_template(X) :- open('index1.html','read', Stream), read_string(Stream,_,X), close(Stream). %:- dynamic counter_u/1, counter_e/1. % % % set counters for quantifier variables to 0 % %:- assert(counter_u(0)). %:- assert(counter_e(0)). % _______ TOP-LEVEL DRIVER __________________________ verify(File) :- catch(verify_core(File), error(vwp_validation(Message),_), format('Validation error: ~w.~n',[Message])), !. verify_core(File) :- retractall(array_type(_,_)), retractall(logic_vars(_)), retractall(context(_)), retractall(contracted_function(_,_,_,_,_,_)), retractall(call_result_counter(_)), assert(call_result_counter(0)), retractall(vc_count(_,_)), assert(vc_count(intraloop,1)), assert(vc_count(exitloop,1)), nl, write('(* Verification Conditions for Alt-Ergo *)'), nl,nl, open(File,read,Stream), lex(Stream,Tokens), parse(Tokens,Triple), prove(Triple), close(Stream), !. verify(_) :- write('...'), nl, nl, write('Syntax error occurred near '), get_context([C|L]), write(C), write('. '), (L \== [] -> write('Full context of error:'), nl,nl, reverse([C|L], Rev), write(Rev) ; true ), !, write('\n\nNote VC-Gen and Alt-Ergo syntax differences:'), nl,nl, write('VC-Gen: function, all, &&, ||, =<, <=>, ==>'), nl, write('Alt-Ergo: logic, forall, and, or, <=, <->, ->'), nl. verify_data(Data) :- catch(verify_data_core(Data), error(vwp_validation(Message),_), format('Validation error: ~w.~n',[Message])), !. verify_data_core(Data) :- retractall(array_type(_,_)), retractall(logic_vars(_)), retractall(context(_)), retractall(contracted_function(_,_,_,_,_,_)), retractall(call_result_counter(_)), assert(call_result_counter(0)), retractall(vc_count(_,_)), assert(vc_count(intraloop,1)), assert(vc_count(exitloop,1)), nl, write('(* Verification Conditions for Alt-Ergo *)'), nl,nl, retractall(array_type(_,_)), open_string(Data,Stream), lex(Stream,Tokens), parse(Tokens,Triple), prove(Triple), close(Stream), !. verify_data(_) :- write('...'), nl, nl, write('Syntax error occurred near '), get_context([C|L]), write(C), write('. '), (L \== [] -> write('Full context of error:'), nl,nl, reverse([C|L], Rev), write(Rev) ; true ), !, write('\n\nNote VC-Gen and Alt-Ergo syntax differences:'), nl,nl, write('VC-Gen: &&, ||, =<, <=>, ==>, all, function'), nl, write('Alt-Ergo: and, or, <=, <->, ->, forall, logic'), nl. get_context(LC) :- findall(C,context(C),L), longest_context(L, LC). longest_context([[C]], [C]). longest_context([C1|L], LC) :- L \== [], length(C1,N), get_max_length(L, N, C1, LC). get_max_length([],_,C,C). get_max_length([Last],N,C,LC) :- !, length(Last,M), (M > N -> LC = Last ; LC = C). %- apropos(Word). get_max_length([Next|L],N,C,LC) :- length(Next,M), (M > N -> get_max_length(L,M,Next,LC) ; get_max_length(L,N,C,LC) ). write_list([H]) :- write(H), !. write_list([H|T]) :- write(H), nl, write_list(T). % ______________________PROVER____________________________ prove(triple(Pre,Stmt,Post)) :- (prove(Pre,Stmt,Post) -> nl ; nl, write('VC generation failed.') ), nl, nl. prove(module(FunctionDefs, Main)) :- prove_function_defs(FunctionDefs), prove(Main). prove_function_defs([]). prove_function_defs([fdef(F,_,_,_,Pre,Post,Body,_)|Rest]) :- normal_function_exit(Body,Post,NormalPost), wp(WP,Body,NormalPost,Post,Post,false), !, theorem(function(F),(Pre ==> WP)), prove_function_defs(Rest). prove(Pre,Stmt,Post) :- normal_function_exit(Stmt,Post,NormalPost), wp(WP,Stmt,NormalPost,Post,Post,false), !, theorem(start,(Pre ==> WP)). % A body containing C-style return statements may not establish its contract % merely by falling off the end. Legacy bodies that assign result directly % retain their original fall-through semantics. normal_function_exit(Body,_,false) :- contains_return(Body), !. normal_function_exit(_,Post,Post). % ________ THE WP PREDICATE: WEAKEST PRECONDITIONS _______ wp(Break, break, _, _, Break, _). wp(Continue, continue, _, _, _, Continue). % Return has its own continuation. In particular, it ignores the ordinary % continuation computed from statements that follow it. wp(Pre, returned(Result,Expr), _, Return, _, _) :- check_subst(Return,Result,Expr,Pre). % A contracted function call is permitted only as the complete right-hand % side of an assignment. FreshResult is declared as an arbitrary logic % constant in the preamble. Validity over all interpretations of that % constant supplies the same universal semantics as an explicit forall. wp(Pre, (X = Call), Post, _, _, _) :- contracted_call(Call, Formals, Result, _ResultType, Requires, Ensures), !, call_parts(Call,_,Actuals), pairs(Formals,Actuals,ParamBindings), subst_many(Requires,ParamBindings,CallRequires), fresh_call_result(Call,FreshResult), subst_many(Ensures,[Result-FreshResult|ParamBindings],CallEnsures), check_subst(Post,X,FreshResult,ReturnPost), Pre = (CallRequires && (CallEnsures ==> ReturnPost)). wp(Pre, (X = Expr), Post, _, _, _) :- check_subst(Post, X, Expr, Pre). wp(Pre, (S ; REST), Post, Return, Break, Continue) :- wp(Inter, REST, Post, Return, Break, Continue), wp(Pre, S, Inter, Return, Break, Continue). wp(((X ==> TR) && (not(X) ==> Post)), if(X, Y), Post, Return, Break, Continue) :- wp(TR, Y, Post, Return, Break, Continue). wp((((X ==> TR) && (not(X) ==> FA))), if(X, Y, Z), Post, Return, Break, Continue) :- wp(TR, Y, Post, Return, Break, Continue), wp(FA, Z, Post, Return, Break, Continue). wp(I, loop(I, B, S), Post, Return, _, _) :- wp(Q, S, I, Return, Post, I), !, theorem(intraloop,((B && I) ==> Q)), theorem(exitloop,((not(B) && I) ==> Post)). wp((B ==> Post), assert(B), Post, _, _, _). % _______________ theorem(Code,T) :- nl, % write('Is the following true? '), theorem2(Code), array_quantifiers, nl, pprin(T,0), !, nl. % write('Enter true./false.: '), read(Inp), % Inp == true. theorem2(intraloop):- retract(vc_count(intraloop,C)), atom_concat('goal intraloop', C, M), atom_concat(M, ':', M2), C1 is C+1, assert(vc_count(intraloop,C1)), write(M2). theorem2(exitloop):- retract(vc_count(exitloop,C)), atom_concat('goal exitloop', C, M), atom_concat(M, ':', M2), C1 is C+1, assert(vc_count(exitloop,C1)), write(M2). theorem2(start):- write('goal start:'). theorem2(function(F)) :- atom_concat('goal function_',F,M), atom_concat(M,':',M2), write(M2). contracted_call(Call,Formals,Result,ResultType,Requires,Ensures) :- call_parts(Call,F,Actuals), contracted_function(F,Formals,Result,ResultType,Requires,Ensures), same_length(Formals,Actuals). call_parts(zero_call(F),F,[]) :- !. call_parts(Call,F,Actuals) :- compound(Call), Call =.. [F|Actuals]. pairs([],[],[]). pairs([F|Fs],[A|As],[F-A|Rest]) :- pairs(Fs,As,Rest). fresh_call_result(_,Fresh) :- retract(call_result_counter(N)), N1 is N+1, assert(call_result_counter(N1)), atomic_list_concat([r,'_',N1],Fresh). % Simultaneous substitution avoids errors in calls such as f(y,x), where % sequential substitutions would accidentally rewrite an actual argument. subst_many(Term,Bindings,Out) :- atomic(Term), !, (memberchk(Term-Replacement,Bindings) -> Out=Replacement ; Out=Term). subst_many(Term,Bindings,Out) :- Term =.. [Op|Args], subst_many_list(Args,Bindings,Args2), Out =.. [Op|Args2]. subst_many_list([],_,[]). subst_many_list([H|T],Bindings,[H2|T2]) :- subst_many(H,Bindings,H2), subst_many_list(T,Bindings,T2). % Every normalized array declaration is stored as a separate array_type/2 % fact. Quantify all of them; selecting only the first fact left later arrays % free in the generated goal (for example, b or olda). array_quantifiers :- forall(array_type(T, L), write_array_quants(T, L)). write_array_quants(_, []). write_array_quants(T, [A|Rest]) :- nl, write('forall '), write(A), write(' : '), write(T), write(' '), write(farray), write('.'), nl, write_array_quants(T, Rest). % __________ SUBSTITUTION: P[V <- E] = Q ___________________ % P[array(A,I) <- E] = Q check_subst(array(A,I), array(A,I), E, E) :- !. check_subst(P, array(A,I), E, Q3) :- !, get_quant_vars(P,Quants), get_sub_vars(P,SubVars,Quants), gen_conj_for_array(SubVars,P,array(A,I),E,L), gen_wp_for_array(L,Neg,Q2), (Q2 \== true -> Q3 = (Q2 && (Neg ==> P)) ; Q3 = P). %simplify_impl(Q3,Q4), %simplify(Q4,Q). check_subst(P,V,E,Q) :- subst(P,V,E,Q). get_quant_vars(all([K],_,_), [K]) :- !. get_quant_vars(all([K,_,L],_,_),[K,L]) :- !. get_quant_vars(exists([K],_,_),[K]) :- !. get_quant_vars(V,[]) :- atomic(V), !. get_quant_vars(P, L) :- P =.. [_|ArgList], get_quant_vars_in(ArgList,L). get_quant_vars_in([],[]). get_quant_vars_in([H|T], L) :- get_quant_vars(H,L1), get_quant_vars_in(T,L2), append(L1,L2,L). get_sub_vars(array(A,I),[array(A,I)],Quants) :- atom(I), \+ member(I,Quants). get_sub_vars(array(A,I),Ans,Quants) :- \+ atom(I), get_vars_in_sub(I,Vs), (check_not_quants(Vs,Quants) -> Ans = [array(A,I)] ; Ans = []). get_sub_vars(V, [],_) :- atomic(V), !. get_sub_vars(P, L, Qs) :- P =.. [_|ArgList], get_sub_vars_in(ArgList,L,Qs). get_sub_vars_in([],[],_). get_sub_vars_in([H|T],L,Qs) :- get_sub_vars(H,L1,Qs), get_sub_vars_in(T,L2,Qs), union(L1,L2,L). check_not_quants([],_). check_not_quants([H|T],Qs) :- \+ member(H,Qs), check_not_quants(T,Qs). get_vars_in_sub(N,[]) :- number(N), !. get_vars_in_sub(V, [V]) :- atom(V), !. get_vars_in_sub(E, L) :- E =.. [_|ArgList], get_vars_in_sub2(ArgList,L). get_vars_in_sub2([],[]). get_vars_in_sub2([H|T],L) :- get_vars_in_sub(H,L1), get_vars_in_sub2(T,L2), append(L1,L2,L). gen_conj_for_array([],_,_,_,[]). gen_conj_for_array([array(B,_)|T],P,array(A,I),E,T2) :- A \== B, !, gen_conj_for_array(T,P,array(A,I),E, T2). gen_conj_for_array([array(A,J)|T],P,array(A,I),E,[Conj|T2]) :- subst(P,array(A,J),E,Q2), Conj = ((I = J) ==> Q2), gen_conj_for_array(T,P,array(A,I),E, T2). gen_wp_for_array([(P==>Q)], not(P), (P==>Q)) :- !. gen_wp_for_array([], true, true). gen_wp_for_array([(P==>Q)|T], not(P)&&P2, (P==>Q)&&T2) :- gen_wp_for_array(T,P2,T2). % ======================================================== simplify_impl((X = X+1) ==> _, true). simplify_impl(not((X = X)) ==> _, true). simplify_impl((X = X) ==> Q, Q2) :- simplify_impl(Q, Q2). simplify_impl(P && Q, R) :- simplify_impl(P, P2), simplify_impl(Q, Q2), simplify_and(P2,Q2,R). simplify_impl((P ==> Q), (P2 ==> Q2)) :- simplify_impl(P, P2), simplify_impl(Q, Q2). simplify_impl(P,P). simplify_and(false,_,false) :- !. simplify_and(_,false,false) :- !. simplify_and(true,Q,Q) :- !. simplify_and(P,true,P) :- !. simplify_and(P,Q,P && Q). % ======================================================== subst(V,V,E,E) :- !. subst(P,V,E,Q) :- P =.. [Op|L], !, subst_list(L,V,E,L2), Q2 =.. [Op|L2], simplify(Q2,Q). subst(A,_,_,A). subst_list([],_,_,[]). subst_list([H|T],V,E,[H2|T2]) :- subst(H,V,E,H2), subst_list(T,V,E,T2). %___________________ PRETTY PRINTING ____________________ pprin_imply_ante(A && B) :- pprin(A,0), write(' and '), pprin_imply_ante(B). pprin_imply_ante(A) :- pprin(A,0). pprin((A && B), N) :- simplify(A,A2), pprin(A2,N), write(' and '), nl, %tabs(N), simplify(B,B2), pprin(B2,N). pprin((A '||' B), N) :- !, simplify(A,A2), simplify(B,B2), tabs(N), pprin_or((A2 '||' B2)), nl. pprin((A <=> B), N) :- !, simplify(A,A2), tabs(N), write('('), pprin(A2,0), write(' <-> '), simplify(B,B2), pprin(B2,0),write(')'), nl. pprin((not(X=X) ==> _), N) :- pprin(true,N), !. pprin(((X=X-1) ==> _), N) :- !, pprin(true,N). pprin(((X=X+1) ==> _), N) :- !, pprin(true,N). pprin(((not(J=J+1)) ==> B), N) :- pprin(B,N). pprin(((X=X) ==> B), N) :- pprin(B,N), !. pprin((A ==> B), N) :- !, simplify(A,A2), tabs(N), write('('), (N \== 0 -> pprin_imply_ante(A2) ; pprin(A2,N)), % newline(A2), write(' -> '), nl, M is N+1, simplify(B,B2), pprin(B2,M), nl, tabs(N), write(')'), nl. pprin(all(Vs, L:H, P), N) :- tabs(N), write('('), write('forall '), write_domain_no_ops(Vs), write(': int. '), simplify(L,L2), simplify(H,H2), write(L2), write( ' <= '), write_inequalities(Vs), write(' <= '), write(H2), write( ' -> '), simplify(P, P2), pprin(P2,0), write(')'). pprin(exists(Vs, L:H, P), N) :- tabs(N), write('('), write('exists '), write_domain_no_ops(Vs), write(': int. '), simplify(L,L2), simplify(H,H2), write(L2), write( ' <= '), write_inequalities(Vs), write(' <= '), write(H2), write( ' and '), simplify(P, P2), pprin(P2,0), write(')'). pprin(forall_typed(V,T,P), N) :- !, tabs(N), write('(forall '), write(V), write(': '), write_base_type(T), write('. '), pprin(P,0), write(')'). pprin(not(not(A)), N) :- !, simplify(A, A2), tabs(N), write_term(A2). pprin(not(A), N) :- !, simplify(not, A, A2), tabs(N), write_term(A2). pprin((X=Y), N) :- !, simplify(X,X2),tabs(N), write_term(X2), write( ' > '), simplify(Y,Y2), write_term(Y2). pprin((X>=Y), N) :- !, simplify(X,X2),tabs(N), write_term(X2), write( ' >= '), simplify(Y,Y2), write_term(Y2). pprin((X==Y), N) :- !, simplify(X,X2),tabs(N), write_term(X2), write(' = '), simplify(Y,Y2), write_term(Y2). pprin((X=Y), N) :- !, simplify(X,X2),tabs(N), write_term(X2), write(' = '), simplify(Y,Y2), write_term(Y2). pprin((X '!=' Y), N) :- !, simplify(X,X2), simplify(Y,Y2), tabs(N), write('not('),write_term(X2),write(=),write_term(Y2),write(')'). pprin(A, N) :- simplify(A, A2), tabs(N), write_term(A2). pprin_or((A '||' B)) :- !, pprin(A,0), write(' or '), pprin(B,0). pprin_or((A && B)) :- !, write_term(A), write(' and '), write_term(B). pprin_or(A) :- pprin(A,0). write_inequalities([V]) :- write(V), !. write_inequalities([V, OP |L]) :- write(V), write_op(OP), write_inequalities(L). write_op('=<') :- !, write( '<= '). write_op('==') :- !, write( '= '). write_op('&&') :- !, write(' and '). write_op('||') :- !, write(' or '). write_op('==>'):- !, write(' -> '). write_op('<=>'):- !, write(' <-> '). write_op(OP) :- write(OP). write_domain_no_ops(Vs) :- extract_vars(Vs, Ws), write_no_ops(Ws). extract_vars([],[]). extract_vars([E],L) :- (check_include(E) -> L = [E] ; L = []). extract_vars([E,_|L],L2) :- (check_include(E) -> L2 = [E|L3] ; L2 = L3), extract_vars(L,L3). write_no_ops([V]) :- write(V). write_no_ops([V|L]) :- write(V), write(', '), write_no_ops(L). check_include(E) :- atom(E), logic_vars(Vs), \+ is_logic_var(Vs,E). is_logic_var([],_) :- fail. is_logic_var([_:Vs | L], E) :- member(E,Vs) ; is_logic_var(L,E). % __________________ WRITE TERM _____________ write_term(A) :- atomic(A), write(A). write_term((A '||' B)) :- !, write_term(A), write(' or '), write_term(B). write_term((A && B)) :- !, write_term(A), write(' and '), write_term(B). write_term(array(A,T)) :- write(A), write('['), write(T), write(']'). write_term(not(T)) :- write('not('), write_term(T), write(')'). write_term((A >= B)) :- write_term(A), write('>='), write_term(B). write_term((A =< B)) :- write_term(A), write('<='), write_term(B). % write_term((A mod B)) :- write-term(A), write('%'), write_term(B). write_term(T) :- T =.. [OP,A1,A2], name(OP, L), (identifier(_,L,[]) -> write(T) ; write('('), write_term(A1), write_op(OP), write_term(A2), write(')') ). write_term(T) :- write(T). tabs(0) :- !. tabs(N) :- write(' '), M is N-1, tabs(M). newline((_ && _)) :- !. newline((_ ==> _)) :- !. newline((_ <=> _)) :- !. newline(_ '||' _) :- !. newline(_) :- nl. %__________________ SIMPLIFICATION RULES _________________ simplify((1-1), 0) :- !. simplify((1*1), 1) :- !. simplify((X+0), X) :- !. simplify((X+1)-1, X) :- !. simplify((X-1)+1, X) :- !. simplify((X+1)=<(Y+1), (X= []. types([(quote:TV):T|L], CL, CL_out) --> [@, type], ['\'', id(TV), id(T)], {CL2 = [type:T | CL], asserta(context(CL2))}, types(L, CL2, CL_out). types([T:EL|L], CL, CL_out) --> [@, type, id(T), =], {CL2 = [type_enum:T | CL], asserta(context(CL2))}, enumeration(EL), types(L, CL2, CL_out). enumeration([N]) --> [id(N)]. enumeration([N|L]) --> [id(N)], ['|'], enumeration(L). write_enumeration([H]) :- !, write(H), nl. write_enumeration([H|T]) :- write(H), write(' | '), write_enumeration(T). write_types([]). write_types([(quote:TV):T|L]) :- !, write(type), write(' '), write('\''), write(TV), write(' '), write(T),nl, write_types(L). write_types([T:EL|L]) :- write(type), write(' '), write(T), write(' = '), write_enumeration(EL), write_types(L). % --------------------- FUNCTIONS ---------------------------- functions([],L,L) --> []. functions([fun(F,D,R)|L],CL, CL_out) --> [@, function, id(F), ':'], domain(D), ['-','>'], base_type(R), !, {CL2 = [function:F|CL], asserta(context(CL2))}, functions(L, CL2, CL_out). functions([fun(F,D)|L], CL, CL_out) --> [@, function, id(F), ':'],domain(D), {CL2 = [function:F|CL], asserta(context(CL2))}, functions(L, CL2, CL_out). domain([T]) --> base_type(T). domain([T|L]) --> base_type(T), [ ','], domain(L). base_type((quote:TV):T) --> ['\'', id(TV), id(T)]. base_type(quote:TV) --> ['\'', id(TV)]. base_type(type_inst(T,T2)) --> [id(T), id(T2)]. base_type(T) --> [id(T)]. write_base_type(T) :- atom(T), write(T). write_base_type(type_inst(T,T2)) :- write(T), write( ' '), write(T2). write_base_type(quote:TV) :- write('\''), write(TV). write_base_type((quote:TV):T) :- write('\''), write(TV), write(' '), write(T). write_domain([E]) :- write_base_type(E), !. write_domain([E|T]) :- write_base_type(E), write(', '), write_domain(T). write_functions([]). write_functions([fun(F,D,R)|L]) :- write(logic), write(' '), write(F), write(' : '), write_domain(D), write(' -> '), write_base_type(R), nl, write_functions(L). write_functions([fun(F,D)|L]) :- write(logic), write(' '), write(F), write(' : '), write_domain(D), nl, write_functions(L). % ---------------- CONTRACTED FUNCTIONS ------------------------- % % Syntax: % @requires ... % @ensures result = ... % int f(int x, int y) { % @var local:int % ... % return ...; % } % % Parameters are passed by value. A contracted call is legal only as the % complete RHS of an assignment: v = f(a,b); contract_functions([],L,L) --> []. contract_functions([fdef(F,Params,Result,ResultType,Pre,Post,Body,Locals)|Rest], CL,CL_out) --> [@,requires], {CL1=[contract|CL], asserta(context(CL1))}, bexpr(RawPre), [@,ensures], bexpr(RawPost), type(ResultType), [id(F), '('], c_parameter_decls(RawParams), [')'], ['{'], vars(RawLocals,CL1,BodyCL), stmts(RawBody,BodyCL,_), ['}'], {scope_function(F,RawParams,RawLocals,RawPre,RawPost,RawBody, Params,Locals,Result,Pre,Post,Body), parameter_names(Params,FormalNames)}, {asserta(contracted_function(F,FormalNames,Result,ResultType,Pre,Post))}, contract_functions(Rest,CL1,CL_out). c_parameter_decls([]) --> []. c_parameter_decls([T:[P]|Rest]) --> type(T), [id(P)], c_parameter_decls_tail(Rest). c_parameter_decls_tail([]) --> []. c_parameter_decls_tail([T:[P]|Rest]) --> [','], type(T), [id(P)], c_parameter_decls_tail(Rest). % Function variables are alpha-renamed internally. Source programs can use % natural local names (including the implicit name result) in every function % without collisions in the generated Alt-Ergo declarations. scope_function(F,RawParams,RawLocals,RawPre,RawPost,RawBody, Params,Locals,Result,Pre,Post,Body) :- parameter_names(RawParams,RawFormalNames), declaration_names(RawLocals,RawLocalNames), append(RawFormalNames,[result|RawLocalNames],SourceNames), scoped_names(F,SourceNames,ScopedNames), pairs(SourceNames,ScopedNames,Bindings), rename_declarations(RawParams,Bindings,Params), rename_declarations(RawLocals,Bindings,Locals), memberchk(result-Result,Bindings), subst_many(RawPre,Bindings,Pre), subst_many(RawPost,Bindings,Post), subst_many(RawBody,Bindings,ScopedBody), rewrite_function_returns(ScopedBody,Result,Body). % Attach every return to the implicit result variable. WP gives returned/2 % a separate continuation, so returns are valid inside branches and loops and % need not be the final statement in the surrounding syntax tree. rewrite_function_returns(Body,Result,Rewritten) :- rewrite_returns(Body,Result,Rewritten). rewrite_returns(return(Expr),Result,returned(Result,Expr)) :- !. rewrite_returns((A;B),Result,(RA;RB)) :- !, rewrite_returns(A,Result,RA), rewrite_returns(B,Result,RB). rewrite_returns(if(Condition,Then),Result,if(Condition,RThen)) :- !, rewrite_returns(Then,Result,RThen). rewrite_returns(if(Condition,Then,Else),Result,if(Condition,RThen,RElse)) :- !, rewrite_returns(Then,Result,RThen), rewrite_returns(Else,Result,RElse). rewrite_returns(loop(Invariant,Condition,Body),Result, loop(Invariant,Condition,RBody)) :- !, rewrite_returns(Body,Result,RBody). rewrite_returns(Statement,_,Statement). contains_return(return(_)) :- !. contains_return(returned(_,_)) :- !. contains_return(Term) :- compound(Term), Term=..[_|Args], contains_return_list(Args). contains_return_list([H|_]) :- contains_return(H), !. contains_return_list([_|T]) :- contains_return_list(T). % Unlike contracted functions, @program has no signature from which a return % type can be obtained. Require an explicit declaration when it returns a % value, e.g. @var result: bool. validate_main_result(Body,Vars) :- (contains_return(Body) -> declaration_names(Vars,Names), (memberchk(result,Names) -> true ; validation_error('a returning main program must declare result')) ; true). scoped_names(_,[],[]). scoped_names(F,[Name|Names],[Scoped|ScopedNames]) :- atomic_list_concat([F,Name],'_',Scoped), scoped_names(F,Names,ScopedNames). rename_declarations([],_,[]). rename_declarations([T:Names|Rest],Bindings,[T:Scoped|ScopedRest]) :- rename_names(Names,Bindings,Scoped), rename_declarations(Rest,Bindings,ScopedRest). rename_names([],_,[]). rename_names([Name|Names],Bindings,[Scoped|ScopedNames]) :- memberchk(Name-Scoped,Bindings), rename_names(Names,Bindings,ScopedNames). parameter_names([],[]). parameter_names([_:[P]|Rest],[P|Names]) :- parameter_names(Rest,Names). collect_function_vars([],[]). collect_function_vars([fdef(_,Params,Result,ResultType,_,_,_,Locals)|Rest],All) :- append(Params,[ResultType:[Result]|Locals],Here), collect_function_vars(Rest,Tail), append(Here,Tail,All). % Collect calls in the same order in which wp/6 visits them. Sequential WP % works backwards, so calls in the rest of a sequence are allocated first. % This keeps each predeclared r_N paired with the return type used by WP. collect_call_result_vars(FunctionDefs,MainBody,Vars) :- collect_function_call_types(FunctionDefs,FunctionTypes), collect_stmt_call_types(MainBody,MainTypes), append(FunctionTypes,MainTypes,Types), number_call_result_vars(Types,1,Vars). collect_function_call_types([],[]). collect_function_call_types([fdef(_,_,_,_,_,_,Body,_)|Rest],Types) :- collect_stmt_call_types(Body,Here), collect_function_call_types(Rest,Tail), append(Here,Tail,Types). collect_stmt_call_types((A;B),Types) :- !, collect_stmt_call_types(B,BTypes), collect_stmt_call_types(A,ATypes), append(BTypes,ATypes,Types). collect_stmt_call_types(if(_,Then),Types) :- !, collect_stmt_call_types(Then,Types). collect_stmt_call_types(if(_,Then,Else),Types) :- !, collect_stmt_call_types(Then,ThenTypes), collect_stmt_call_types(Else,ElseTypes), append(ThenTypes,ElseTypes,Types). collect_stmt_call_types(loop(_,_,Body),Types) :- !, collect_stmt_call_types(Body,Types). collect_stmt_call_types((_ = Call),[ResultType]) :- contracted_call(Call,_,_,ResultType,_,_), !. collect_stmt_call_types(_,[]). number_call_result_vars([],_,[]). number_call_result_vars([Type|Types],N,[Type:[Name]|Vars]) :- atomic_list_concat([r,'_',N],Name), N1 is N+1, number_call_result_vars(Types,N1,Vars). write_call_result_vars([]). write_call_result_vars([Type:[Name]|Vars]) :- write(logic), write(' '), write(Name), write(': '), write_call_result_type(Type), nl, write_call_result_vars(Vars). write_call_result_type(arr(Type)) :- !, write_base_type(Type), write(' farray'). write_call_result_type(Type) :- write_base_type(Type). normalize_vars(Vars,Normalized) :- normalize_vars(Vars,[],Rev), reverse(Rev,Normalized). normalize_vars([],Acc,Acc). normalize_vars([T:Names|Rest],Acc,Out) :- add_var_names(Names,T,Acc,Acc2), normalize_vars(Rest,Acc2,Out). add_var_names([],_,Acc,Acc). add_var_names([Name|Names],Type,Acc,Out) :- (member(OtherType:OtherNames,Acc), memberchk(Name,OtherNames) -> (OtherType == Type -> Acc2=Acc ; format('Type error: variable ~w has conflicting types.~n',[Name]), fail) ; Acc2=[Type:[Name]|Acc]), add_var_names(Names,Type,Acc2,Out). validate_module(LogicFunctions,FunctionDefs,MainBody) :- function_names(FunctionDefs,Names), sort(Names,Unique), length(Names,N), length(Unique,UniqueN), (N =:= UniqueN -> true ; validation_error('contracted function names must be unique')), (\+ (member(fun(F,_,_),LogicFunctions), memberchk(F,Names)), \+ (member(fun(F,_),LogicFunctions), memberchk(F,Names)) -> true ; validation_error('a contracted function conflicts with a logic function')), validate_function_bodies(FunctionDefs,Names,Edges), validate_stmt(MainBody,main,Names,_), (recursive_edge(Edges) -> validation_error('recursive and mutually recursive function calls are not allowed') ; true). validation_error(Message) :- throw(error(vwp_validation(Message),_)). function_names([],[]). function_names([fdef(F,_,_,_,_,_,_,_)|Rest],[F|Names]) :- function_names(Rest,Names). validate_function_bodies([],_,[]). validate_function_bodies([fdef(F,Params,Result,_,Pre,Post,Body,Locals)|Rest],Names,Edges) :- validate_function_signature(Params,Result,Locals), no_contracted_call(Pre,Names), no_contracted_call(Post,Names), parameter_names(Params,FormalNames), declaration_names(Locals,LocalNames), validate_function_writes(Body,FormalNames,[Result|LocalNames]), validate_stmt(Body,F,Names,Here), validate_function_bodies(Rest,Names,Tail), append(Here,Tail,Edges). validate_function_signature(Params,Result,Locals) :- parameter_names(Params,FormalNames), sort(FormalNames,UniqueFormals), length(FormalNames,N), length(UniqueFormals,N2), (N =:= N2 -> true ; validation_error('function parameter names must be unique')), (memberchk(Result,FormalNames) -> validation_error('the result variable must differ from all parameters') ; true), declaration_names(Locals,LocalNames), (member(Name,LocalNames), memberchk(Name,[Result|FormalNames]) -> validation_error('local variables must not shadow parameters or the result') ; true). declaration_names([],[]). declaration_names([_:Names|Rest],All) :- declaration_names(Rest,Tail), append(Names,Tail,All). validate_stmt((A;B),Owner,Names,Edges) :- !, validate_stmt(A,Owner,Names,E1), validate_stmt(B,Owner,Names,E2), append(E1,E2,Edges). validate_stmt(if(C,T),Owner,Names,Edges) :- !, no_contracted_call(C,Names), validate_stmt(T,Owner,Names,Edges). validate_stmt(if(C,T,E),Owner,Names,Edges) :- !, no_contracted_call(C,Names), validate_stmt(T,Owner,Names,E1), validate_stmt(E,Owner,Names,E2), append(E1,E2,Edges). validate_stmt(loop(I,C,B),Owner,Names,Edges) :- !, no_contracted_call(I,Names), no_contracted_call(C,Names), validate_stmt(B,Owner,Names,Edges). validate_stmt(assert(C),_,Names,[]) :- !, no_contracted_call(C,Names). validate_stmt(return(_),main,_,[]) :- !, validation_error('return is allowed only inside a function'). validate_stmt(returned(_,Expr),_,Names,[]) :- !, no_contracted_call(Expr,Names). validate_stmt((L=R),Owner,Names,Edges) :- !, no_contracted_call(L,Names), (call_parts(R,F,Args), memberchk(F,Names) -> (atom(L) -> true ; validation_error('a function result must be assigned to a simple variable')), contracted_function(F,Formals,_,_,_,_), (same_length(Formals,Args) -> true ; validation_error('wrong number of arguments in a function call')), no_contracted_calls_list(Args,Names), Edges=[Owner-F] ; no_contracted_call(R,Names), Edges=[]). validate_stmt(break,_,_,[]) :- !. validate_stmt(continue,_,_,[]) :- !. validate_stmt(Other,_,Names,[]) :- no_contracted_call(Other,Names). % Parameters are read-only, including array parameters. Functions may write % only their result and declared locals, so calls have no hidden global effect. validate_function_writes((A;B),Params,Writable) :- !, validate_function_writes(A,Params,Writable), validate_function_writes(B,Params,Writable). validate_function_writes(if(_,T),Params,Writable) :- !, validate_function_writes(T,Params,Writable). validate_function_writes(if(_,T,E),Params,Writable) :- !, validate_function_writes(T,Params,Writable), validate_function_writes(E,Params,Writable). validate_function_writes(loop(_,_,B),Params,Writable) :- !, validate_function_writes(B,Params,Writable). validate_function_writes((L=_),Params,Writable) :- !, lhs_root(L,Root), (memberchk(Root,Params) -> validation_error('function parameters are read-only') ; memberchk(Root,Writable) -> true ; validation_error('functions may assign only their result and local variables')). validate_function_writes(_, _, _). lhs_root(array(A,_),A) :- !. lhs_root(array(A,_,_),A) :- !. lhs_root(A,A). no_contracted_calls_list([],_). no_contracted_calls_list([H|T],Names) :- no_contracted_call(H,Names), no_contracted_calls_list(T,Names). no_contracted_call(Term,_) :- atomic(Term), !. no_contracted_call(zero_call(F),Names) :- !, (memberchk(F,Names) -> validation_error('function calls are allowed only as variable = function(arguments)') ; true). no_contracted_call(Term,Names) :- Term=..[F|Args], (memberchk(F,Names) -> validation_error('function calls are allowed only as variable = function(arguments)') ; no_contracted_calls_list(Args,Names)). recursive_edge(Edges) :- member(F-_,Edges), reachable_call(F,F,Edges,[]), !. reachable_call(Start,Current,Edges,Visited) :- member(Current-Next,Edges), (Next == Start ; \+ memberchk(Next,Visited), reachable_call(Start,Next,Edges,[Current|Visited])). % ---------------------------- AXIOMS ------------------------------- axioms([], L,L) --> []. axioms([A:TQB|L],CL,CL_out) --> [@, axiom, id(A), ':'], {CL2 = [axiom:A|CL], asserta(context(CL2))}, typed_bexpr(TQB), axioms(L,CL2,CL_out). typed_bexpr(TQ:B) --> type_quantifiers(TQ), bexpr(B). type_quantifiers([]) --> []. type_quantifiers([DL:T | L]) --> [all], ids(DL), [:], base_type(T), ['.'], type_quantifiers(L). write_type_quantifiers([]). write_type_quantifiers([DL:T | L]) :- write(forall), write(' '), write_comma_list(DL), write(': '), write_base_type(T), write('. '), write_type_quantifiers(L). write_axioms([]). write_axioms([A:(TQ:B)|L]) :- write(axiom), write(' '), write(A), write(': '), write_type_quantifiers(TQ), pprin(B,0), nl, write_axioms(L). /* You may have to do it recursively in general write_func_body((L==>R)) :- !, write(L), write(' -> '), write(R). write_func_body((L<=>R)) :- !, write(L), write(' <-> '), write(R). write_func_body((L'||'R)) :- !, write(L), write(' or '), write(R). write_func_body((L&&R)) :- !, write(L), write(' and '), write(R). write_func_body(B) :- write(B). */ % --------------------- PROGRAM DECLARATIONS ---------------- type(T) --> [id(T)]. type(arr(T)) --> [id(T),'[]']. %type(mat(T)) --> [id(T), '[]', '[]']. type(type_inst(T1,T2)) --> [id(T1), id(T2)]. vars([], L, L) --> []. vars([T:Vs|L], CL, CL_out) --> [@, X], {X == var; X = vars}, {CL2 = [var_decl|CL], asserta(context(CL2))}, ids(Vs), [:], type(T), vars(L,CL2,CL_out). ids([I]) --> [id(I)]. ids([I|L]) --> [id(I), ','], ids(L). write_comma_list([H]) :- write(H), !. write_comma_list([H|T]) :- write(H), write(','), write(' '), write_comma_list(T). write_vars([]). write_vars([arr(T):L1 | L]) :- !, assert(array_type(T,L1)), write_vars(L). write_vars([T:L1 | L]) :- write(logic), write(' '), write_comma_list(L1), write(': '), write_base_type(T), nl, write_vars(L). % C-like structs deprecated % % types([T|L]) --> [@, type, id(N), '{'], % fields(F), {T=..[N|F]}, types(L). % % fields([F:T]) --> type(T), [id(F), ';', '}']. % fields([F:T | L]) --> type(T), [id(F), ';'], fields(L). % cmpdstmt AND OTHER STATEMENTS % --------------------- PROGRAM CONTROL STRUCTURES -------------------- stmts((S1 ; S), CL_in, CL_out) --> stmt(S1, CL_in, CL2), stmts(S, CL2, CL_out). stmts(S, CL_in, CL_out) --> stmt(S, CL_in, CL_out). stmt(S, CL_in, CL_out) --> ifthenelse(S, CL_in, CL_out). stmt(S, CL_in, CL_out) --> while(S, CL_in, CL_out). stmt(break, CL, CL) --> [break], [';']. stmt(continue, CL, CL) --> [continue], [';']. stmt(return(E), CL, CL) --> [return], expr(E), [';']. stmt(return(E), CL, CL) --> [return], bexpr(E), [';']. stmt(S, CL_in, CL_out) --> assert(S, CL_in, CL_out). stmt(S, CL_in, CL_out) --> cmpdstmt(S, CL_in, CL_out). stmt(S, CL_in, CL_out) --> assign(S, CL_in, CL_out), [;]. stmt(S, CL_in, CL_out) --> proc_call(S, CL_in, CL_out), [;]. cmpdstmt(S, CL_in, CL_out) --> ['{'], stmts(S, CL_in, CL_out), ['}']. assign((L = R), CL_in, CL_out) --> var(L), [=], expr(R), {CL_out = [assign|CL_in], asserta(context(CL_out))}. assign((L = R), CL_in, CL_out) --> var(L), [=], bexpr(R), {CL_out = [assign|CL_in], asserta(context(CL_out))}. proc_call(S, CL_in, CL_out) --> [id(X)], ['('], {CL_out = [call:X|CL_in], asserta(context(CL_out))}, exprlist(L), [')'], {S =.. [X|L]}. ifthenelse(if(B,Then), CL_in, CL_out) --> [if, '('], {CL2 = [if|CL_in], asserta(context(CL2))}, bexpr(B), [')'], stmt(Then, CL2, CL_out). ifthenelse(if(B,Then,Else), CL_in, CL_out) --> [if, '('], {CL2 = [if|CL_in], asserta(context(CL2))}, bexpr(B), [')'], stmt(Then, CL2, CL3), [else], {CL4 = [else|CL3], asserta(context(CL4))}, stmt(Else,CL4,CL_out). while(loop(I,B,W), CL_in, CL_out) --> [@,invariant], {CL2 = [invariant|CL_in], asserta(context(CL2))}, bexpr(I), [while], ['('], {CL3 = [while|CL2], asserta(context(CL3))}, bexpr(B), [')'], stmt(W,CL3,CL_out). assert(assert(B), CL_in, CL_out) --> [@, assert], {CL_out = [assert|CL_in], asserta(context(CL_out))}, bexpr(B). % _______________ EXPRESSION GRAMMAR (expr and bexpr) bexpr(T) --> imply_expr(T). imply_expr(T) --> or_expr(T1), ['<=='], or_expr(T2), {T =.. ['<==', T1, T2]}. imply_expr(T) --> or_expr(T1), ['==>'], or_expr(T2), {T =.. ['==>', T1, T2]}. imply_expr(T) --> or_expr(T1), ['<=>'], or_expr(T2), {T =.. ['<=>', T1, T2]}. imply_expr(T) --> or_expr(T). or_expr(T) --> and_term(T1), or_expr2(T1, T). or_expr2(T,T) --> []. or_expr2(T1,T) --> ['||'], and_term(T2), or_expr2((T1 '||' T2),T). and_term(T) --> not_term(T1), and_term2(T1,T). and_term2(T,T) --> []. and_term2(T1,T) --> ['&&'], not_term(T2), and_term2((T1 && T2),T). not_term(not(T)) --> [not], ['('], bexpr(T), [')']. not_term(true) --> [true]. not_term(false) --> [false]. not_term(T) --> [all, '('], inequalities(L), [ ','], expr(From), [:], expr(To), [','], bexpr(B), [')'], {T = all(L,From:To,B)}. % {change_quant(all(V,From:To,B), T)}. not_term(T) --> [exists, '('], inequalities(L), [ ','], expr(From), [:], expr(To), [','], bexpr(B), [')'], {T = exists(L,From:To,B)}. % {change_quant(exists(V,From:To,B), T)}. not_term(T) --> [all, '('], [id(V), ','], bexpr(B), [')'], {T = all(V,B)}. % {change_quant(all(V,From:To,B), T)}. not_term(T) --> [exists, '('], [id(V), ','], bexpr(B), [')'], {T = exists(V,B)}. % {change_quant(exists(V,From:To,B), T)}. not_term(T) --> ['('], bexpr(T), [')']. not_term(T) --> rel_expr(T). not_term(T) --> var(T). % boolean variable rel_expr(T) --> expr(T1), [ROP], rel_expr2(T2), {rel_op(ROP), T =.. [ROP,T1,T2]}. rel_expr2(T) --> expr(T). rel_expr2(T) --> expr(T1), [ROP], rel_expr2(T2), {rel_op(ROP), T =.. [ROP,T1,T2]}. rel_op('!='). rel_op('=='). rel_op(=). rel_op(>). rel_op(<). rel_op(=<). rel_op(>=). rel_op('~>'). inequalities([E]) --> expr(E). inequalities([E, OP |L]) --> expr(E), [OP], {member(OP, [<, >, '=<', '>=', =, '=='])}, inequalities(L). % ____________________________ expr(T) --> term(T1), termX(T1, T). termX(T1,T) --> [OP], {member(OP, [+,-])}, term(T2), {T3 =.. [OP,T1,T2]}, termX(T3,T). termX(T,T) --> []. term(T) --> factor(T1), termY(T1, T). termY(T1,T) --> [OP], {operator(OP), \+ member(OP, [+,-])}, factor(T2), {T3 =.. [OP,T1,T2]}, termY(T3,T). termY(T,T) --> []. factor(null) --> [null]. factor([]) --> ['[]']. factor(true) --> [true]. factor(false) --> [false]. factor(X) --> int(X). factor(T) --> var(T). factor(T) --> ['('], expr(T), [')']. int(X) --> [num(X)]. %int(X) --> [id(X)]. var(zero_call(X)) --> [id(X)], ['('], [')']. var(T2) --> [id(X)], ['('], exprlist(L), [')'], {T2=..[X|L]}. var(T) --> [id(X)], ['['], expr(T1), [']'], {T=array(X,T1)}. var(T) --> [id(X)], ['['], expr(T1), [','], expr(T2), [']'], {T=array(X,T1,T2)}. var(X) --> [id(X)]. exprlist([]) --> []. exprlist([E]) --> expr(E). exprlist([E|L]) --> expr(E), [','], exprlist(L). operator('@'). operator('%'). operator(+). operator(-). operator(/). operator(*). operator(:). operator('::'). operator('~>'). % ______________________ LEXICAL ANALYZER ________________________ lex(Stream,Tokens) :- get_chars(Stream,L,0), tokenize(L,Tokens), !. get_chars(Str,L,N) :- get_code(Str,C), get_chars(Str,C,L,N). get_chars(Str, 45, [45|L], N) :- !, get_code(Str,C), (C==45 -> L = [45] ; L = [C|L2], M is N+1, get_chars(Str, L2, M) ). % 45 = - get_chars(Str,C, [C|L1],N) :- (N < 10000 -> M is N+1, get_chars(Str,L1,M) ; asserta(context([end_of_program])), fail ). tokenize([], []). tokenize([47,47|L], L3) :- skip_comment(L,L2), tokenize(L2,L3). %47 = / tokenize([C|L], L3) :- white(C), skip_whites(L,L2), tokenize(L2,L3). tokenize([C|L], [X|L3]) :- alpha(C), identifier(X,[C|L],L2), tokenize(L2,L3). tokenize([C|L], [X|L3]) :- d09(C), digits(X,[C|L],L2), tokenize(L2,L3). tokenize(L, [X|L3]) :- special(X,L,L2), tokenize(L2,L3). skip_whites([], []). skip_whites([C|L], L2) :- (white(C) -> skip_whites(L,L2); L2 = [C|L]). skip_comment([10|L],L) :- !. skip_comment([_|L],L2) :- skip_comment(L,L2). white(9). % tab white(10). % newline white(32). % blank white(13). % Mac CR special('<==', [60,61,61|L],L). special('==>', [61,61,62|L],L). special('<=>', [60,61,62|L],L). special('~>', [126,62|L], L). special('==',[61,61|L],L). special(=<,[61,60|L],L). special(>=,[62,61|L],L). special('!=',[33,61|L],L). special('&&', [38,38|L],L). special('||', [124,124|L],L). special('|', [124|L], L). special('::',[58,58|L],L). special('[]',[91,93|L], L). special(>,[62|L],L). special(=,[61|L],L). special(<,[60|L],L). special('{',[123|L],L). special('}',[125|L],L). special('(',[40|L],L). special(')',[41|L],L). special('[',[91|L],L). special(']',[93|L],L). special(;,[59|L],L). special(:,[58|L],L). special(',',[44|L],L). special(*,[42|L],L). special(+,[43|L],L). special('--', [45,45|L], L). special(-,[45|L],L). special(.,[46|L],L). special(/,[47|L],L). special('@', [64|L], L). special('%', [37|L], L). special('\'',[39|L], L). special('_', [95|L], L). identifier(X) --> ident(L), {name(N,L), (keyword(N) -> X=N; X=id(N))}. ident([X|L]) --> letter(X), legits(L). ident([X]) --> letter(X). legits([X|W]) --> legit(X), legits(W). legits([X]) --> legit(X). legit(X) --> letter(X) ; digit(X). letter(X) --> [X], {alpha(X)}. alpha(X) :- X > 64, X < 91. alpha(X) :- X > 96, X < 123. keyword(true). keyword(false). keyword(not). keyword(if). keyword(else). keyword(while). keyword(program). keyword(break). keyword(requires). keyword(ensures). keyword(invariant). keyword(all). keyword(exists). keyword(null). keyword(axiom). keyword(var). keyword(vars). keyword(type). keyword(continue). keyword(return). keyword(function). keyword(axiom). keyword(assert). keyword(end). digits(num(N)) --> digs(L), {name(N,L)}. digs([X|L]) --> digit(X), digs(L). digs([X]) --> digit(X). digit(X) --> [X], {d09(X)}. d09(X) :- X > 47, X < 58. % ___________ QUANTIFIER RENAMING: NOT USED ___________________ %change_quant2(T,U) :- % change_quant(T,U), !. %change_quant2(T,U) :- % T =.. [OP|Args], % change_list(Args,Args2), % U =.. [OP|Args2]. % %change_list([],[]). %change_list([H|T],[H2|T2]) :- % change_quant2(H,H2), % change_list(T,T2). % %change_quant(all,L,T) :- !, % T1 =.. [all|L], % change_quant(T1,T). %change_quant(exists,L,T) :- !, % T1 =.. [exists|L], % change_quant(T1,T). %change_quant(X,L,T1) :- % T1 =.. [X|L]. % %change_quant(all(V,T1,T2),all(V2,U1,U2)) :- % new_sym(u,V2), % subst(T1,V,V2,U1), % subst(T2,V,V2,U2). %change_quant(exists(V,T1,T2),exists(V2,U1,U2)) :- % new_sym(e,V2), % subst(T1,V,V2,U1), % subst(T2,V,V2,U2). % %new_sym(A, B) :- % inc_counter_for(A, I), % user_concat_atom_number(A, I, B). % %user_concat_atom_number(Atom, N, AN) :- % number_codes(N, Ncodes), % atom_codes(Natom, Ncodes), % atom_concat(Atom, Natom, AN). % %inc_counter_for(u, I) :- % counter_u(Current), % write('Asserted '), write(counter_u(Current)),nl, % I is Current + 1, % retractall(counter_u(_)), % asserta(counter_u(I)), !. % %inc_counter_for(e, I) :- % counter_e(Current), % write('Asserted '), write(counter_e(Current)),nl, % I is Current + 1, % retractall(counter_e(_)), % asserta(counter_e(I)), !. % ====================== CHAT GPT CODE =========================== % :- use_module(library(process)). % :- use_module(library(browse)). % Change these paths if needed node_path('C:/Program Files/nodejs/node.exe'). proxy_script_path('C:/alt-ergo-proxy/server.js'). vcgen_html_path('C:/Users/bhara/OneDrive/Documents/Desktop/VC-GEN/Examples/index1.html'). %% Entry point vcgen_server :- server(8000), start_proxy_once. % open_vcgen_browser. %% Open VCGen HTML page in browser %open_vcgen_browser :- %vcgen_html_path(Path), %atomic_list_concat(['file:///', Path], URL), %format('Opening VCGen interface at ~w~n', [URL]), %browse(URL). %% Start proxy server if not already running start_proxy_once :- already_running_alt_ergo_proxy -> writeln('✅ Alt-Ergo proxy is already running.'); start_alt_ergo_proxy. %% Check if Node.js process is running already_running_alt_ergo_proxy :- process_create(path(tasklist), ['/FI', 'IMAGENAME eq node.exe'], [stdout(pipe(Out))]), read_string(Out, _, String), close(Out), sub_string(String, _, _, _, "node.exe"). %% Start the proxy server start_alt_ergo_proxy :- node_path(Node), proxy_script_path(Script), format('🚀 Launching Alt-Ergo proxy via ~w ~w~n', [Node, Script]), process_create(Node, [Script], [detached(true)]), sleep(1), % give it a moment to start writeln('✅ Alt-Ergo proxy launched.'). %% Kill all node.exe processes (use with care!) stop_proxy :- writeln('🛑 Stopping Node.js processes...'), process_create(path(taskkill), ['/F', '/IM', 'node.exe'], []).