Commit 35bffb50 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

arm.mlw: documentation and todo

parent cb490e22
......@@ -84,6 +84,20 @@ module ARM
end
(*
@@ logic separation (fp : int) = a+10 < fp-24
main:
@@ assume separation fp
.L2:@@ invariant ...
.L3:
.L4:@@ invariant ...
*)
module InsertionSortExample
use import module ARM
......
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