% 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(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. % 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_unix_daemon)). :- use_module(library(http/http_parameters)). :- use_module(library(memfile)). :- public save_file/3. :- http_handler(root(.), get_gui, []). :- http_handler(root(vcgen), get_gui, []). :- http_handler(root(upload), upload, []). :- http_handler(root(verify), call_verify, []). % swipl -O --goal=start_server --stand_alone=true -o vcgen -c vcgen.pl %=====> WORKS ONLY IN LINUX!! % swipl vcgen.pl :- initialization(start_daemon, main). start_daemon :- http_daemon([port(8081), workers(30)]). %====== start_server :- server(8080). server(Port) :- http_server(http_dispatch, [port(Port)]). %-- get_gui(_Request) :- get_template(X), format('Content-type: text/html~n~n'), format(X, [' ',' ']). upload(Request) :- multipart_post_request(Request), !, http_read_data(Request, [file=Data], []), get_template(X), format('Content-type: text/html~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~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). % _______ TOP-LEVEL DRIVER __________________________ verify(File) :- retractall(array_type(_,_)), retractall(logic_vars(_)), retractall(context(_)), 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) :- retractall(array_type(_,_)), retractall(logic_vars(_)), retractall(context(_)), nl, write('(* Verification Conditions for Alt-Ergo *)'), nl,nl, retractall(array_type/2), 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). 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(Pre,Stmt,Post) :- wp(WP,Stmt,Post,Post,false), !, theorem(start,(Pre ==> WP)). % ________ THE WP PREDICATE: WEAKEST PRECONDITIONS _______ wp(Break, break, _, Break, _). wp(Continue, continue, _, _, Continue). wp(Pre, (X = Expr), Post, _, _) :- subst(Post, X, Expr, Pre). wp(Pre, (S ; REST), Post, Break, Continue) :- wp(Inter, REST, Post, Break, Continue), wp(Pre, S, Inter, Break, Continue). wp(((X ==> TR) && (not(X) ==> Post)), if(X, Y), Post, Break, Continue) :- wp(TR, Y, Post, Break, Continue). wp((((X ==> TR) && (not(X) ==> FA))), if(X, Y, Z), Post, Break, Continue) :- wp(TR, Y, Post, Break, Continue), wp(FA, Z, Post, Break, Continue). wp(I, loop(I, B, S), Post, _, _) :- wp(Q, S, I, Post, I), !, theorem(intra,((B && I) ==> Q)), theorem(exit,((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(intra):- write('goal intra_loop:'). theorem2(exit) :- write('goal exit:'). theorem2(start):- write('goal start:'). array_quantifiers :- array_type(T, L), % dynamic predicate write_array_quants(T, L). array_quantifiers. 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 ___________________ 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((A && B), N) :- !, simplify(A,A2), pprin(A2,N), write(' and '), nl, simplify(B,B2), pprin(B2,N). % , newline(B2). 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((A ==> B), N) :- !, simplify(A,A2), tabs(N), write('('), pprin(A2,0), % newline(A2), write(' ->'), nl, M is N+1, simplify(B,B2), pprin(B2,M), 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(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= 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(array(A,T)) :- write(A), write('['), write(T), write(']'). write_term(not(T)) :- write('not('), write_term(T), write(')'). write_term((A =< B)) :- write(A), write('<='), write(B). write_term((A mod B)) :- write(A), write('%'), write(B). write_term(T) :- T =.. [OP,A1,A2], name(OP, L), (identifier(_,L,[]) -> write(T) ; write('('), write_term(A1), write(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(Ts,[], TL), functions(Fs,TL, FL), axioms(As, FL, AL), precondition(Pre, AL, PreCL), postcondition(Post, PreCL,PostCL), [@, program], vars(Vs, PostCL, VL), stmts(ParseTree, VL, _), [@, end], eop, {write_preamble(Ts,Fs,As,Vs)}. precondition(Pre,In,[requires|In]) --> [@, requires], {asserta(context([requires|In]))}, bexpr(Pre). postcondition(Post,In,[ensures|In]) --> [@, ensures], {asserta(context([ensures|In]))}, bexpr(Post). eop --> ['--']. write_preamble(Ts,Fs,As,Vs) :- write_types(Ts), write_functions(Fs), write_axioms(As), nl, write_vars(Vs), assert(logic_vars(Vs)). % ---------------- TYPES -------------------------------- types([], L, L) --> []. 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). % ---------------------------- 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) --> [@, var], {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(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(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('~>'). % ______________________ 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(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 ___________________ %:- dynamic counter_u/1, counter_e/1. % set counters for quantifier variables to 0 %:- assert(counter_u(0)). %:- assert(counter_e(0)). %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)), !.