Commit 714395e8 authored by MARCHE Claude's avatar MARCHE Claude

trywhy3: fix examples

parent 6cb890ee
......@@ -1093,7 +1093,7 @@ module Impl
(* Technically speaking, the entry point of the main loop.
Should be called with a preprocessed set of formula
independent of the interpretation (no free variable),
and a empty unificator (identity substitution). *)
and a empty unifier (identity substitution). *)
with extend_branch (base:nlimpl_fo_formula_list)
(tab:nlimpl_tableau)
......
module Fact
module FactWhile
use import mach.int.Int
use import int.Fact
use import ref.Ref
(** Factorial with a while loop *)
let fact_imp (x:int) : int
requires { x >= 0 }
ensures { result = fact x }
......@@ -20,3 +21,23 @@ module Fact
let main () = (fact_imp 7, fact_imp 42)
end
module FactFor
use import mach.int.Int
use import int.Fact
use import ref.Ref
(** Factorial with a for loop *)
let fact_imp (x:int) : int
requires { x >= 0 }
ensures { result = fact x }
= let r = ref 1 in
for y = 1 to x do
invariant { !r = fact (y-1) }
r := !r * !y
done;
!r
let main () = (fact_imp 7, fact_imp 42)
end
......@@ -171,9 +171,12 @@
<div title="Console" id="console">
</div>
</div>
<script defer="true" src="ace-builds/src-noconflict/ace.js" type="text/javascript" charset="utf-8"></script>
<script defer="true" type="text/javascript" src="editor_helper.js" ></script>
<script defer="true" type="text/javascript" src="trywhy3.js" ></script>
<script defer="true" src="ace-builds/src-noconflict/ace.js"
type="text/javascript" charset="utf-8"></script>
<script defer="true" type="text/javascript"
src="editor_helper.js"></script>
<script defer="true" type="text/javascript"
src="trywhy3.js"></script>
</body>
</html>
......@@ -8,7 +8,7 @@ module M
let isqrt (x:int) : int
requires { x >= 0 }
ensures { result >= 0 }
ensures { result <= x < sqr (result + 1) }
ensures { sqr result <= x < sqr (result + 1) }
= let count = ref 0 in
let sum = ref 1 in
while !sum <= x do
......
......@@ -231,20 +231,22 @@ let why3_execute (modules,_theories) =
with Not_found -> acc)
modules []
in
let s =
List.sort
(fun (l1,_) (l2,_) -> Loc.compare l2 l1)
mods
in
Html.ul (List.rev_map snd s)
match mods with
| [] -> Html.par [Html.of_string "No main function found"]
| _ ->
let s =
List.sort
(fun (l1,_) (l2,_) -> Loc.compare l2 l1)
mods
in
Html.ul (List.rev_map snd s)
(* Connecting Why3 calls to the interface *)
let temp_file_name = "/input.mlw"
let () =
Sys_js.register_file ~name:temp_file_name ~content:""
let () = Sys_js.register_file ~name:temp_file_name ~content:""
let run_why3 f lang global text =
let ch = open_out temp_file_name in
......@@ -271,21 +273,28 @@ let run_why3 f lang global text =
"unexpected exception: %a (%s)" Exn_printer.exn_printer e
(Printexc.to_string e))]
let add_why3_cmd buttonname f lang =
let add_why3_cmd buttonname f input_lang =
let handler = Dom.handler
(fun _ev ->
log "why3 prove is running";
let global = Js.Unsafe.global in
let editor = Js.Unsafe.get global (Js.string "editor") in
let lang =
Js.to_string
(Js.Unsafe.meth_call editor "getAttribute"
[| Js.Unsafe.inject (Js.string "lang") |])
in
let code = Js.to_string (Js.Unsafe.meth_call editor "getValue" [| |]) in
let answer = run_why3 f lang global code in
(* remove the previous answer if any *)
log ("Why3 is running, lang = " ^ lang);
let answer = run_why3 f input_lang global code in
log "Why3 answer given";
let console =
get_opt (Dom_html.document ## getElementById (Js.string "console"))
in
(* remove the previous answer if any *)
Js.Opt.iter (console##lastChild) (Dom.removeChild console);
(* put the new answer *)
Dom.appendChild console answer;
(* give the focus back to the editor *)
ignore (Js.Unsafe.meth_call editor "focus" [| |]);
Js._false)
in
......
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