Commit 32cc8bf5 authored by Johannes Kanig's avatar Johannes Kanig

Merge remote-tracking branch 'lri/master' into why3server

parents 05b5fbd3 39a17763
......@@ -280,14 +280,19 @@ pvsbin/
/modules/mach/int/
# Try Why3
/src/trywhy3/trywhy3.js
/src/trywhy3/trywhy3.byte
/src/trywhy3/trywhy3.js
/src/trywhy3/alt_ergo_worker.byte
/src/trywhy3/alt_ergo_worker.js
/src/trywhy3/why3_worker.byte
/src/trywhy3/why3_worker.js
/src/trywhy3/index.en.html
/src/trywhy3/index.fr.html
/src/trywhy3/index.html
/src/trywhy3/ace-builds
/src/trywhy3/ace-builds/
/src/trywhy3/*.png
/src/trywhy3/alt-ergo-1.00-private-2015-01-29
/src/trywhy3/fontawesome/
# jessie3
/src/jessie/config.log
......
......@@ -1523,10 +1523,10 @@ ALTERGOMODS=util/numsNumbers util/numbers \
instances/matching \
sat/sat_solvers \
main/frontend
ALTERGOCMO=$(addprefix $(ALTERGODIR)/src/, $(addsuffix .cmo,$(ALTERGOMODS)))
TRYWHY3CMO=lib/why3/why3.cma
TRYWHY3CMO=lib/why3/why3.cma $(addprefix $(ALTERGODIR)/src/, $(addsuffix .cmo,$(ALTERGOMODS)))
trywhy3: src/trywhy3/trywhy3.js src/trywhy3/index.en.html src/trywhy3/index.fr.html
trywhy3: src/trywhy3/trywhy3.js src/trywhy3/why3_worker.js src/trywhy3/alt_ergo_worker.js src/trywhy3/index.en.html src/trywhy3/index.fr.html
%.fr.html: %.prehtml
yamlpp -l fr $< -o $@
......@@ -1535,19 +1535,38 @@ trywhy3: src/trywhy3/trywhy3.js src/trywhy3/index.en.html src/trywhy3/index.fr.h
yamlpp -l en $< -o $@
src/trywhy3/trywhy3.js: src/trywhy3/trywhy3.byte
js_of_ocaml --extern-fs -I . -I src/trywhy3 --file=trywhy3.conf:/ \
--file=try_alt_ergo.drv:/ \
js_of_ocaml --extern-fs -I . -I src/trywhy3 \
--file=drinkers.why:/ \
--file=simplearith.why:/ \
--file=bin_mult.mlw:/ \
--file=fact.mlw:/ \
--file=isqrt.mlw:/ \
`find theories modules \( -name "*.mlw" -o -name "*.why" \) -printf " --file=%p:/"` \
+weak.js +nat.js $^
src/trywhy3/trywhy3.byte: $(TRYWHY3CMO) src/trywhy3/trywhy3.cmo
src/trywhy3/trywhy3.byte: src/trywhy3/worker_proto.cmo src/trywhy3/trywhy3.cmo
$(JSOCAMLC) $(BFLAGS) -o $@ -linkpkg $(BLINKFLAGS) $^
src/trywhy3/why3_worker.js: src/trywhy3/why3_worker.byte
js_of_ocaml --extern-fs -I . -I src/trywhy3 --file=trywhy3.conf:/ \
--file=try_alt_ergo.drv:/ \
`find theories modules \( -name "*.mlw" -o -name "*.why" \) -printf " --file=%p:/"` \
+weak.js +nat.js $^
src/trywhy3/why3_worker.byte: $(TRYWHY3CMO) src/trywhy3/worker_proto.cmo src/trywhy3/why3_worker.cmo
$(JSOCAMLC) $(BFLAGS) -o $@ -linkpkg $(BLINKFLAGS) $^
src/trywhy3/alt_ergo_worker.js: src/trywhy3/alt_ergo_worker.byte
js_of_ocaml +weak.js +nat.js +dynlink.js +toplevel.js $^
src/trywhy3/alt_ergo_worker.byte: $(ALTERGOCMO) src/trywhy3/worker_proto.cmo src/trywhy3/alt_ergo_worker.cmo
$(JSOCAMLC) $(BFLAGS) -o $@ -linkpkg $(BLINKFLAGS) $^
src/trywhy3/alt_ergo_worker.cmo: src/trywhy3/worker_proto.cmo
src/trywhy3/why3_worker.cmo: src/trywhy3/worker_proto.cmo
src/trywhy3/trywhy3.cmo: src/trywhy3/worker_proto.cmo
src/trywhy3/%.cmo: src/trywhy3/%.ml
$(JSOCAMLC) $(BFLAGS) -c $<
......@@ -1555,7 +1574,11 @@ src/trywhy3/%.cmi: src/trywhy3/%.mli
$(JSOCAMLC) $(BFLAGS) -c $<
clean::
rm -f src/trywhy3/trywhy3.js src/trywhy3/trywhy3.byte
rm -f src/trywhy3/trywhy3.js src/trywhy3/trywhy3.byte src/trywhy3/trywhy3.cm* \
src/trywhy3/why3_worker.js src/trywhy3/why3_worker.byte src/trywhy3/why3_worker.cm* \
src/trywhy3/alt_ergo_worker.js src/trywhy3/alt_ergo_worker.byte src/trywhy3/alt_ergo_worker.cm* \
src/trywhy3/worker_proto.cm* \
src/trywhy3/index.en.html src/trywhy3/index.fr.html
CLEANDIRS += src/trywhy3
......
This diff is collapsed.
This diff is collapsed.
......@@ -5,30 +5,29 @@ module McCarthy91
use import int.Int
function spec (x: int) : int = if x <= 100 then 91 else x-10
(* traditional recursive implementation *)
let rec f91 (n:int) : int variant { 101-n }
ensures { result = if n <= 100 then 91 else n - 10 }
ensures { result = spec n }
= if n <= 100 then
f91 (f91 (n + 11))
else
n - 10
(* non-recursive implementation using a while loop *)
use import ref.Ref
function f (x: int) : int = if x <= 100 then 91 else x-10
(* iter k x = f^k(x) *)
clone import int.Iter with type t = int, function f = f
clone import int.Iter with type t = int, function f = spec
let f91_nonrec (n0: int) ensures { result = f n0 }
let f91_nonrec (n0: int) ensures { result = spec n0 }
= let e = ref 1 in
let n = ref n0 in
while !e > 0 do
invariant { !e >= 0 /\ iter !e !n = f n0 }
invariant { !e >= 0 /\ iter !e !n = spec n0 }
variant { 101 - !n + 10 * !e, !e }
if !n > 100 then begin
n := !n - 10;
......@@ -40,4 +39,40 @@ module McCarthy91
done;
!n
(* Use a 'morally' irrelevant control flow from a recursive function
to ease proof (the recursive structure does not contribute to the
program execution). This is a technique for proving derecursified
programs. See verifythis_2016_tree_traversal for a more
complex example. *)
exception Stop
let f91_pseudorec (n0:int) : int
ensures { result = spec n0 }
= let e = ref 1 in
let n = ref n0 in
let bloc () : unit
requires { !e >= 0 }
ensures { !(old e) > 0 }
ensures { if !(old n) > 100 then !n = !(old n) - 10 /\ !e = !(old e) - 1
else !n = !(old n) + 11 /\ !e = !(old e) + 1 }
raises { Stop -> !e = !(old e) = 0 /\ !n = !(old n) }
= if not (!e > 0) then raise Stop;
if !n > 100 then begin
n := !n - 10;
e := !e - 1
end else begin
n := !n + 11;
e := !e + 1
end
in
let rec aux () : unit
requires { !e > 0 }
variant { 101 - !n }
ensures { !e = !(old e) - 1 /\ !n = spec !(old n) }
raises { Stop -> false }
= let u = !n in bloc (); if u <= 100 then (aux (); aux ()) in
try aux (); bloc (); absurd
with Stop -> !n end
end
......@@ -2,57 +2,17 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC3" version="2.4.1" timelimit="10" memlimit="0"/>
<prover id="2" name="Z3" version="3.2" timelimit="10" memlimit="0"/>
<prover id="3" name="veriT" version="201310" timelimit="5" memlimit="4000"/>
<prover id="4" name="Alt-Ergo" version="0.99.1" timelimit="10" memlimit="0"/>
<prover id="0" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../mccarthy.mlw" expanded="true">
<theory name="McCarthy91" sum="fc4723c0574acd30d3d960beb8743bed" expanded="true">
<goal name="WP_parameter f91" expl="VC for f91" expanded="true">
<proof prover="0" timelimit="2"><result status="valid" time="0.00"/></proof>
<proof prover="2" timelimit="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4" timelimit="2"><result status="valid" time="0.02" steps="11"/></proof>
<theory name="McCarthy91" sum="4a73db0e7cb62d49c98fa874799f159d" expanded="true">
<goal name="WP_parameter f91" expl="VC for f91">
<proof prover="0"><result status="valid" time="0.00" steps="15"/></proof>
</goal>
<goal name="WP_parameter f91_nonrec" expl="VC for f91_nonrec" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter f91_nonrec.1" expl="1. loop invariant init" expanded="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4"><result status="valid" time="0.01" steps="1"/></proof>
</goal>
<goal name="WP_parameter f91_nonrec.2" expl="2. loop invariant preservation" expanded="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4"><result status="valid" time="0.00" steps="22"/></proof>
</goal>
<goal name="WP_parameter f91_nonrec.3" expl="3. loop variant decrease" expanded="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4"><result status="valid" time="0.01" steps="6"/></proof>
</goal>
<goal name="WP_parameter f91_nonrec.4" expl="4. loop invariant preservation" expanded="true">
<proof prover="0"><result status="valid" time="0.03"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4"><result status="valid" time="0.24" steps="87"/></proof>
</goal>
<goal name="WP_parameter f91_nonrec.5" expl="5. loop variant decrease" expanded="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4"><result status="valid" time="0.01" steps="6"/></proof>
</goal>
<goal name="WP_parameter f91_nonrec.6" expl="6. postcondition" expanded="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="5"/></proof>
</goal>
</transf>
<goal name="WP_parameter f91_nonrec" expl="VC for f91_nonrec">
<proof prover="0"><result status="valid" time="0.11" steps="171"/></proof>
</goal>
<goal name="WP_parameter f91_pseudorec" expl="VC for f91_pseudorec">
<proof prover="0"><result status="valid" time="0.02" steps="44"/></proof>
</goal>
</theory>
</file>
......
This diff is collapsed.
This diff is collapsed.
Instructions to build TryWhy3
-----------------------------
* in subdirectory src/trywhy3/ do
** install 'ace'
git clone https://github.com/ajaxorg/ace-builds.git
** copy the fontawesome webfont locally :
mkdir fontawesome
cd fontawesome
wget -nd https://www.lri.fr/~kn/trywhy3/fontawesome/fontawesome.css
wget -nd https://www.lri.fr/~kn/trywhy3/fontawesome/fontawesome-webfont.woff
** install Alt-Ergo
- get sources of Alt-Ergo and put them in directory src/trywhy3/ e.g. in
src/trywhy3/alt-ergo-1.00-private-2015-01-29/
- apply the patch alt-ergo.patch
cd <alt-ergo dir>
patch -p1 < ../alt-ergo.patch
- compile Alt-Ergo
./configure
make byte
* in the main directory
** if necessary, change the following line of Makefile.in to point
to Alt-Ergo sources
ALTERGODIR=src/trywhy3/alt-ergo-1.00-private-2015-01-29
** compile with
make trywhy3
* install : TODO
Only in alt-ergo-1.00-private-2015-01-29/: autom4te.cache
Only in alt-ergo-1.00-private-2015-01-29/: config.status
Only in alt-ergo-1.00-private-2015-01-29/: .depend
Only in alt-ergo-1.00-private-2015-01-29/: Makefile.configurable
diff -c -r /tmp/alt-ergo-1.00-private-2015-01-29/src/sat/sat_solvers.ml alt-ergo-1.00-private-2015-01-29/src/sat/sat_solvers.ml
*** /tmp/alt-ergo-1.00-private-2015-01-29/src/sat/sat_solvers.ml 2016-04-07 16:01:57.449020746 +0200
--- alt-ergo-1.00-private-2015-01-29/src/sat/sat_solvers.ml 2016-04-08 10:26:05.485174395 +0200
***************
*** 23,28 ****
--- 23,30 ----
open Options
open Format
+ exception StepsLimitReached
+
module type S = sig
type t
***************
*** 492,499 ****
--- 494,504 ----
if steps_bound () <> -1
&& Int64.compare !steps (Int64.of_int (steps_bound ())) > 0 then
begin
+ raise StepsLimitReached;
+ (*
printf "Steps limit reached: %Ld@." !steps;
exit 1
+ *)
end;
{ env with tbox = tbox; unit_tbox = utbox; inst = inst }
diff -c -r /tmp/alt-ergo-1.00-private-2015-01-29/src/sat/sat_solvers.mli alt-ergo-1.00-private-2015-01-29/src/sat/sat_solvers.mli
*** /tmp/alt-ergo-1.00-private-2015-01-29/src/sat/sat_solvers.mli 2016-04-07 16:01:57.449020746 +0200
--- alt-ergo-1.00-private-2015-01-29/src/sat/sat_solvers.mli 2016-04-08 10:26:05.485174395 +0200
***************
*** 20,25 ****
--- 20,27 ----
(* This file is distributed under the terms of the CeCILL-C licence *)
(******************************************************************************)
+ exception StepsLimitReached
+
module type S = sig
type t
diff -c -r /tmp/alt-ergo-1.00-private-2015-01-29/src/util/numbers.ml alt-ergo-1.00-private-2015-01-29/src/util/numbers.ml
*** /tmp/alt-ergo-1.00-private-2015-01-29/src/util/numbers.ml 2016-04-07 16:01:57.453020790 +0200
--- alt-ergo-1.00-private-2015-01-29/src/util/numbers.ml 2016-04-08 10:41:51.037337014 +0200
***************
*** 20,28 ****
(* This file is distributed under the terms of the CeCILL-C licence *)
(******************************************************************************)
! module MyZarith = ZarithNumbers
module MyNums = NumsNumbers
! include MyZarith
--- 20,29 ----
(* This file is distributed under the terms of the CeCILL-C licence *)
(******************************************************************************)
! (* module MyZarith = ZarithNumbers *)
module MyNums = NumsNumbers
! include MyNums
!
open Format
open Worker_proto
module SAT = (val (Sat_solvers.get_current ()) : Sat_solvers.S)
module FE = Frontend.Make (SAT)
let print_status fmt _d status steps =
match status with
| FE.Unsat _dep ->
fprintf fmt "Proved (%Ld steps)" steps
| FE.Inconsistent -> ()
(* fprintf fmt "Inconsistent assumption" *)
| FE.Unknown _t | FE.Sat _t ->
fprintf fmt "Unknown (%Ld steps)@." steps
let report_status report _d status _steps =
match status with
| FE.Unsat _dep -> report Valid
| FE.Inconsistent -> ()
| FE.Unknown _t | FE.Sat _t -> report (Unknown "unknown")
let run_alt_ergo_on_task text =
let lb = Lexing.from_string text in
(* from Alt-Ergo, src/main/frontend.ml *)
let a = Why_parser.file Why_lexer.token lb in
Parsing.clear_parser ();
let ltd, _typ_env = Why_typing.file false Why_typing.empty_env a in
match Why_typing.split_goals ltd with
| [d] ->
let d = Cnf.make (List.map (fun (f, _env) -> f, true) d) in
SAT.reset_steps ();
let stat = ref (Invalid "no answer from Alt-Ergo") in
let f s = stat := s in
begin
try
let _x = Queue.fold (FE.process_decl (report_status f))
(SAT.empty (), true, Explanation.empty) d
in
!stat
with Sat_solvers.StepsLimitReached -> Unknown "steps limit reached"
end
| _ -> Invalid "zero or more than 1 goal to solve"
let () =
Options.set_steps_bound 100;
Worker.set_onmessage (fun msg ->
let (id, text) = unmarshal msg in
let result = run_alt_ergo_on_task text in
Worker.post_message (marshal (id,result)))
......@@ -40,6 +40,7 @@
</div>
</div>
<!-- the main page -->
<div id="header">
<div align="right">
<#fr><a href="index.en.html">English version</a></#fr>
<#en><a href="index.fr.html">Version fran&ccedil;aise</a></#en>
......@@ -72,6 +73,7 @@
<#fr>utilis&eacute; pour produire cette page</#fr>
</ul>
</p>
</div>
<div class="menu-bar">
<ul>
<li><a href="#"><#en>File</#en><#fr>Fichier</#fr></a>
......@@ -132,6 +134,10 @@
<li><a href="#" id="prove">
<#en>Prove</#en>
<#fr>Prouver</#fr>
</a></li>
<li><a href="#" id="stop">
<#en>Stop Alt-ergo</#en>
<#fr>Arrêter Alt-ergo</#fr>
</a></li>
</ul>
</li>
......
@import url(fontawesome/fontawesome.css);
/* fontawesome */
[class*="fontawesome-"]:before {
font-family: 'FontAwesome', sans-serif;
}
body {
padding:0;
margin:0;
......@@ -132,20 +140,20 @@ body {
#console ul {
list-style-type: none;
padding: 8px;
margin: 4px;
padding: 0.5em;
/*margin: 0.5em; */
}
#console ul ul {
list-style-type: disc;
padding: 8px;
margin: 4px;
padding: 0.5em;
/*margin: 0.5em;*/
}
#console ul ul ul {
list-style-type: none;
padding: 0px;
margin: 4px;
padding: 0.5em;
/*margin: 0.5em; */
}
#editor {
......@@ -198,3 +206,17 @@ body {
#confirm-dialog .btn {
width:40%;
}
#header {
height: 30vh;
}
.menu-bar {
height: 5vh;
}
#editor-panel {
height: 65vh;
}
#console {
overflow: auto;
}
\ No newline at end of file
This diff is collapsed.
This diff is collapsed.
type command = ParseBuffer of string
| ExecuteBuffer of string
| Init
type output = Error of string (* msg *)
| ErrorLoc of ((int*int*int*int) * string) (* loc * msg *)
| Tasks of ((string * string) (* Theory (id, name) *)
* (string * string) (* Task (id, name *)
* (string * string * string)) (* VC (id, expl, code ) *)
| Result of string list
type prover_answer = Valid | Unknown of string | Invalid of string
let marshal a =
Js.string (String.escaped (Marshal.to_string a [Marshal.No_sharing; Marshal.Compat_32]))
let unmarshal a =
Marshal.from_string (Scanf.unescaped (Js.to_string a)) 0
let log s = ignore (Firebug.console ## log (Js.string s))
let log_time s =
let date = jsnew Js.date_now () in
let date_str = string_of_float ((date ## getTime ()) /. 1000.) in
log (date_str ^ " : " ^ s)
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment