Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
c13b1932
Commit
c13b1932
authored
Aug 24, 2015
by
Léon Gondelman
Browse files
converted standard library and drivers
parent
8dd0e736
Changes
6
Hide whitespace changes
Inline
Side-by-side
bench/bench
View file @
c13b1932
...
...
@@ -46,9 +46,9 @@ drivers () {
if
[[
$f
==
drivers/ocaml
*
.drv
]]
;
then continue
;
fi
echo
-n
"
$f
... "
# running Why
if
!
echo
"theory Test goal G : 1=2 end"
|
$pgm
-F
why
--driver
$f
-
>
/dev/null 2>&1
;
then
if
!
echo
"theory Test goal G : 1=2 end"
|
$pgm
-F
why
ml
--driver
$f
-
>
/dev/null 2>&1
;
then
echo
"why FAILED"
echo
"theory Test goal G : 1=2 end"
|
$pgm
-F
why
--driver
$f
-
echo
"theory Test goal G : 1=2 end"
|
$pgm
-F
why
ml
--driver
$f
-
exit
1
fi
echo
"ok"
...
...
bench/programs/bad-typing/at2.mlw
deleted
100644 → 0
View file @
8dd0e736
module M
use import int.Int
use import ref.Ref
let test (a: (ref int, int)) =
'L:
let (r,_) = a in
r := !r + 1;
assert { let (x, _) = a in !x = (at !x 'L) + 1 }
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../../.. bench/programs/bad-typing/at2"
End:
*)
drivers/alt_ergo_0.93.drv
View file @
c13b1932
...
...
@@ -10,10 +10,3 @@ theory BuiltIn
meta "eliminate_algebraic" "keep_enums"
meta "printer_option" "no_type_cast"
end
(*
Local Variables:
mode: why
compile-command: "make -C .. bench"
End:
*)
drivers/pvs-common.gen
View file @
c13b1932
...
...
@@ -263,7 +263,7 @@ end
theory list.Mem
syntax predicate mem "member(%1, %2)"
end
theory list.Nth
...
...
@@ -297,30 +297,29 @@ theory set.Set
syntax function empty "(emptyset :: %t0)"
syntax predicate is_empty "empty?(%1)"
remove prop empty_def
1
remove prop empty_def
syntax function add "add(%1, %2)"
remove prop add_def
1
remove prop add_def
syntax function singleton "singleton(%1)"
syntax function remove "remove(%1, %2)"
remove prop remove_def
1
remove prop remove_def
remove prop subset_remove
syntax function union "union(%1, %2)"
remove prop union_def
1
remove prop union_def
syntax function inter "intersection(%1, %2)"
remove prop inter_def
1
remove prop inter_def
syntax function diff "difference(%1, %2)"
remove prop diff_def
1
remove prop diff_def
remove prop subset_diff
(* TODO: choose *)
syntax function all "fullset"
remove prop all_def
end
theory set.Fset
...
...
@@ -334,24 +333,24 @@ theory set.Fset
syntax function empty "(emptyset :: %t0)"
syntax predicate is_empty "empty?(%1)"
remove prop empty_def
1
remove prop empty_def
syntax function add "add(%1, %2)"
remove prop add_def
1
remove prop add_def
syntax function singleton "singleton(%1)"
syntax function remove "remove(%1, %2)"
remove prop remove_def
1
remove prop remove_def
remove prop subset_remove
syntax function union "union(%1, %2)"
remove prop union_def
1
remove prop union_def
syntax function inter "intersection(%1, %2)"
remove prop inter_def
1
remove prop inter_def
syntax function diff "difference(%1, %2)"
remove prop diff_def
1
remove prop diff_def
remove prop subset_diff
(* TODO: choose *)
...
...
modules/mach/array.mlw
View file @
c13b1932
...
...
@@ -8,31 +8,32 @@
module Array32
use import int.Int
use import mach.int.Int32
use import map.Map as M
type array 'a model { length: int32; mutable elts: map int 'a }
invariant { 0 <= to_int self.length }
type array 'a = private {
mutable ghost elts : map int 'a;
length : int32;
} invariant { 0 <= to_int length }
function get (a: array
~
'a) (i: int) : 'a =
M.get
a.elts i
let ghost
function get
_unsafe
(a: array 'a) (i: int) : 'a = a.elts i
function set (a: array
~
'a) (i: int) (v: 'a) : array 'a
=
{ a with
elts = M.set a.elts i v }
val ghost
function set
_unsafe
(a: array 'a) (i: int) (v: 'a) : array 'a
ensures { result.
elts = M.set a.elts i v
/\ result.length = a.length
}
(** syntactic sugar *)
function ([]) (a: array 'a) (i: int) : 'a = get a i
function ([<-]) (a: array 'a) (i: int) (v: 'a) : array 'a = set a i v
function ([]) (a: array 'a) (i: int) : 'a = get
_unsafe
a i
function ([<-]) (a: array 'a) (i: int) (v: 'a) : array 'a = set
_unsafe
a i v
val ([]) (a: array
~
'a) (i: int32) : 'a
val ([]) (a: array 'a) (i: int32) : 'a
requires { "expl:index in array bounds" 0 <= to_int i < to_int a.length }
ensures { result = a[to_int i] }
val ([]<-) (a: array
~
'a) (i: int32) (v: 'a) : unit writes {a}
val ([]<-) (a: array 'a) (i: int32) (v: 'a) : unit writes {a}
requires { "expl:index in array bounds" 0 <= to_int i < to_int a.length }
ensures { a.elts = M.set (old a.elts) (to_int i) v }
val length (a: array ~'a) : int32 ensures { result = a.length }
(** unsafe get/set operations with no precondition *)
exception OutOfBounds
...
...
@@ -50,31 +51,28 @@ module Array32
= if i < of_int 0 || i >= length a then raise OutOfBounds;
a[i] <- v
function make (n: int32) (v: ~'a) : array 'a =
{ length = n; elts = M.const v }
val make (n: int32) (v: ~'a) : array 'a
val function make (n: int32) (v: 'a) : array 'a
requires { "expl:array creation size" to_int n >= 0 }
ensures { result
= make n v
}
ensures { result
.elts = M.const v /\ result.length = n
}
val append (a1: array
~
'a) (a2: array 'a) : array 'a
val append (a1: array 'a) (a2: array 'a) : array 'a
ensures { to_int result.length = to_int a1.length + to_int a2.length }
ensures { forall i:int. 0 <= i < to_int a1.length -> result[i] = a1[i] }
ensures { forall i:int. 0 <= i < to_int a2.length ->
result[to_int a1.length + i] = a2[i] }
val sub (a: array
~
'a) (ofs: int32) (len: int32) : array 'a
val sub (a: array 'a) (ofs: int32) (len: int32) : array 'a
requires { 0 <= to_int ofs /\ 0 <= to_int len }
requires { to_int ofs + to_int len <= to_int a.length }
ensures { result.length = len }
ensures { forall i:int. 0 <= i < to_int len ->
result[i] = a[to_int ofs + i] }
val copy (a: array
~
'a) : array 'a
val copy (a: array 'a) : array 'a
ensures { result.length = a.length }
ensures { forall i:int. 0 <= i < to_int result.length -> result[i] = a[i] }
let
fill (a: array
~
'a) (ofs: int32) (len: int32) (v: 'a)
val
fill (a: array 'a) (ofs: int32) (len: int32) (v: 'a)
: unit
requires { 0 <= to_int ofs /\ 0 <= to_int len }
requires { to_int ofs + to_int len <= to_int a.length }
ensures { forall i:int.
...
...
@@ -82,18 +80,8 @@ module Array32
to_int ofs + to_int len <= i < to_int a.length) -> a[i] = (old a)[i] }
ensures { forall i:int. to_int ofs <= i < to_int ofs + to_int len ->
a[i] = v }
= 'Init:
for k = 0 to Int.(-) (to_int len) 1 do (* FIXME: for loop on int32 *)
invariant { forall i:int.
(0 <= i < to_int ofs \/
to_int ofs + to_int len <= i < to_int a.length) ->
a[i] = (at a 'Init)[i] }
invariant { forall i:int. to_int ofs <= i < to_int ofs + k -> a[i] = v }
let k = of_int k in
a[ofs + k] <- v
done
val blit (a1: array ~'a) (ofs1: int32)
val blit (a1: array 'a) (ofs1: int32)
(a2: array 'a) (ofs2: int32) (len: int32) : unit writes {a2}
requires { 0 <= to_int ofs1 /\ 0 <= to_int len }
requires { to_int ofs1 + to_int len <= to_int a1.length }
...
...
@@ -107,7 +95,7 @@ module Array32
to_int ofs2 <= i < to_int ofs2 + to_int len ->
a2[i] = a1[to_int ofs1 + i - to_int ofs2] }
val self_blit (a: array
~
'a) (ofs1: int32) (ofs2: int32) (len: int32) : unit
val self_blit (a: array 'a) (ofs1: int32) (ofs2: int32) (len: int32) : unit
writes {a}
requires { 0 <= to_int ofs1 /\ 0 <= to_int len /\
to_int ofs1 + to_int len <= to_int a.length }
...
...
@@ -125,31 +113,32 @@ end
module Array31
use import int.Int
use import mach.int.Int31
use import map.Map as M
type array 'a model { length: int31; mutable elts: map int 'a }
invariant { 0 <= to_int self.length }
type array 'a = private {
mutable ghost elts : map int 'a;
length : int31;
} invariant { 0 <= to_int length }
function get (a: array
~
'a) (i: int) : 'a =
M.get
a.elts i
let ghost
function get
_unsafe
(a: array 'a) (i: int) : 'a = a.elts i
function set (a: array
~
'a) (i: int) (v: 'a) : array 'a
=
{ a with
elts = M.set a.elts i v }
val ghost
function set
_unsafe
(a: array 'a) (i: int) (v: 'a) : array 'a
ensures { result.
elts = M.set a.elts i v
/\ result.length = a.length
}
(** syntactic sugar *)
function ([]) (a: array 'a) (i: int) : 'a = get a i
function ([<-]) (a: array 'a) (i: int) (v: 'a) : array 'a = set a i v
function ([]) (a: array 'a) (i: int) : 'a = get
_unsafe
a i
function ([<-]) (a: array 'a) (i: int) (v: 'a) : array 'a = set
_unsafe
a i v
val ([]) (a: array
~
'a) (i: int31) : 'a
val ([]) (a: array 'a) (i: int31) : 'a
requires { "expl:index in array bounds" 0 <= to_int i < to_int a.length }
ensures { result = a[to_int i] }
val ([]<-) (a: array
~
'a) (i: int31) (v: 'a) : unit writes {a}
val ([]<-) (a: array 'a) (i: int31) (v: 'a) : unit writes {a}
requires { "expl:index in array bounds" 0 <= to_int i < to_int a.length }
ensures { a.elts = M.set (old a.elts) (to_int i) v }
val length (a: array ~'a) : int31 ensures { result = a.length }
(** unsafe get/set operations with no precondition *)
exception OutOfBounds
...
...
@@ -167,31 +156,28 @@ module Array31
= if i < of_int 0 || i >= length a then raise OutOfBounds;
a[i] <- v
function make (n: int31) (v: ~'a) : array 'a =
{ length = n; elts = M.const v }
val make (n: int31) (v: ~'a) : array 'a
val function make (n: int31) (v: 'a) : array 'a
requires { "expl:array creation size" to_int n >= 0 }
ensures { result
= make n v
}
ensures { result
.elts = M.const v /\ result.length = n
}
val append (a1: array
~
'a) (a2: array 'a) : array 'a
val append (a1: array 'a) (a2: array 'a) : array 'a
ensures { to_int result.length = to_int a1.length + to_int a2.length }
ensures { forall i:int. 0 <= i < to_int a1.length -> result[i] = a1[i] }
ensures { forall i:int. 0 <= i < to_int a2.length ->
result[to_int a1.length + i] = a2[i] }
val sub (a: array
~
'a) (ofs: int31) (len: int31) : array 'a
val sub (a: array 'a) (ofs: int31) (len: int31) : array 'a
requires { 0 <= to_int ofs /\ 0 <= to_int len }
requires { to_int ofs + to_int len <= to_int a.length }
ensures { result.length = len }
ensures { forall i:int. 0 <= i < to_int len ->
result[i] = a[to_int ofs + i] }
val copy (a: array
~
'a) : array 'a
val copy (a: array 'a) : array 'a
ensures { result.length = a.length }
ensures { forall i:int. 0 <= i < to_int result.length -> result[i] = a[i] }
let
fill (a: array
~
'a) (ofs: int31) (len: int31) (v: 'a)
val
fill (a: array 'a) (ofs: int31) (len: int31) (v: 'a)
: unit
requires { 0 <= to_int ofs /\ 0 <= to_int len }
requires { to_int ofs + to_int len <= to_int a.length }
ensures { forall i:int.
...
...
@@ -199,18 +185,8 @@ module Array31
to_int ofs + to_int len <= i < to_int a.length) -> a[i] = (old a)[i] }
ensures { forall i:int. to_int ofs <= i < to_int ofs + to_int len ->
a[i] = v }
= 'Init:
for k = 0 to Int.(-) (to_int len) 1 do (* FIXME: for loop on int31 *)
invariant { forall i:int.
(0 <= i < to_int ofs \/
to_int ofs + to_int len <= i < to_int a.length) ->
a[i] = (at a 'Init)[i] }
invariant { forall i:int. to_int ofs <= i < to_int ofs + k -> a[i] = v }
let k = of_int k in
a[ofs + k] <- v
done
val blit (a1: array ~'a) (ofs1: int31)
val blit (a1: array 'a) (ofs1: int31)
(a2: array 'a) (ofs2: int31) (len: int31) : unit writes {a2}
requires { 0 <= to_int ofs1 /\ 0 <= to_int len }
requires { to_int ofs1 + to_int len <= to_int a1.length }
...
...
@@ -224,7 +200,7 @@ module Array31
to_int ofs2 <= i < to_int ofs2 + to_int len ->
a2[i] = a1[to_int ofs1 + i - to_int ofs2] }
val self_blit (a: array
~
'a) (ofs1: int31) (ofs2: int31) (len: int31) : unit
val self_blit (a: array 'a) (ofs1: int31) (ofs2: int31) (len: int31) : unit
writes {a}
requires { 0 <= to_int ofs1 /\ 0 <= to_int len /\
to_int ofs1 + to_int len <= to_int a.length }
...
...
@@ -242,31 +218,32 @@ end
module Array63
use import int.Int
use import mach.int.Int63
use import map.Map as M
type array 'a model { length: int63; mutable elts: map int 'a }
invariant { 0 <= to_int self.length }
type array 'a = private {
mutable ghost elts : map int 'a;
length : int63;
} invariant { 0 <= to_int length }
function get (a: array
~
'a) (i: int) : 'a =
M.get
a.elts i
let ghost
function get
_unsafe
(a: array 'a) (i: int) : 'a = a.elts i
function set (a: array
~
'a) (i: int) (v: 'a) : array 'a
=
{ a with
elts = M.set a.elts i v }
val ghost
function set
_unsafe
(a: array 'a) (i: int) (v: 'a) : array 'a
ensures { result.
elts = M.set a.elts i v
/\ result.length = a.length
}
(** syntactic sugar *)
function ([]) (a: array 'a) (i: int) : 'a = get a i
function ([<-]) (a: array 'a) (i: int) (v: 'a) : array 'a = set a i v
function ([]) (a: array 'a) (i: int) : 'a = get
_unsafe
a i
function ([<-]) (a: array 'a) (i: int) (v: 'a) : array 'a = set
_unsafe
a i v
val ([]) (a: array
~
'a) (i: int63) : 'a
val ([]) (a: array 'a) (i: int63) : 'a
requires { "expl:index in array bounds" 0 <= to_int i < to_int a.length }
ensures { result = a[to_int i] }
val ([]<-) (a: array
~
'a) (i: int63) (v: 'a) : unit writes {a}
val ([]<-) (a: array 'a) (i: int63) (v: 'a) : unit writes {a}
requires { "expl:index in array bounds" 0 <= to_int i < to_int a.length }
ensures { a.elts = M.set (old a.elts) (to_int i) v }
val length (a: array ~'a) : int63 ensures { result = a.length }
(** unsafe get/set operations with no precondition *)
exception OutOfBounds
...
...
@@ -284,31 +261,28 @@ module Array63
= if i < of_int 0 || i >= length a then raise OutOfBounds;
a[i] <- v
function make (n: int63) (v: ~'a) : array 'a =
{ length = n; elts = M.const v }
val make (n: int63) (v: ~'a) : array 'a
val function make (n: int63) (v: 'a) : array 'a
requires { "expl:array creation size" to_int n >= 0 }
ensures { result
= make n v
}
ensures { result
.elts = M.const v /\ result.length = n
}
val append (a1: array
~
'a) (a2: array 'a) : array 'a
val append (a1: array 'a) (a2: array 'a) : array 'a
ensures { to_int result.length = to_int a1.length + to_int a2.length }
ensures { forall i:int. 0 <= i < to_int a1.length -> result[i] = a1[i] }
ensures { forall i:int. 0 <= i < to_int a2.length ->
result[to_int a1.length + i] = a2[i] }
val sub (a: array
~
'a) (ofs: int63) (len: int63) : array 'a
val sub (a: array 'a) (ofs: int63) (len: int63) : array 'a
requires { 0 <= to_int ofs /\ 0 <= to_int len }
requires { to_int ofs + to_int len <= to_int a.length }
ensures { result.length = len }
ensures { forall i:int. 0 <= i < to_int len ->
result[i] = a[to_int ofs + i] }
val copy (a: array
~
'a) : array 'a
val copy (a: array 'a) : array 'a
ensures { result.length = a.length }
ensures { forall i:int. 0 <= i < to_int result.length -> result[i] = a[i] }
let
fill (a: array
~
'a) (ofs: int63) (len: int63) (v: 'a)
val
fill (a: array 'a) (ofs: int63) (len: int63) (v: 'a)
: unit
requires { 0 <= to_int ofs /\ 0 <= to_int len }
requires { to_int ofs + to_int len <= to_int a.length }
ensures { forall i:int.
...
...
@@ -316,18 +290,8 @@ module Array63
to_int ofs + to_int len <= i < to_int a.length) -> a[i] = (old a)[i] }
ensures { forall i:int. to_int ofs <= i < to_int ofs + to_int len ->
a[i] = v }
= 'Init:
for k = 0 to Int.(-) (to_int len) 1 do (* FIXME: for loop on int63 *)
invariant { forall i:int.
(0 <= i < to_int ofs \/
to_int ofs + to_int len <= i < to_int a.length) ->
a[i] = (at a 'Init)[i] }
invariant { forall i:int. to_int ofs <= i < to_int ofs + k -> a[i] = v }
let k = of_int k in
a[ofs + k] <- v
done
val blit (a1: array ~'a) (ofs1: int63)
val blit (a1: array 'a) (ofs1: int63)
(a2: array 'a) (ofs2: int63) (len: int63) : unit writes {a2}
requires { 0 <= to_int ofs1 /\ 0 <= to_int len }
requires { to_int ofs1 + to_int len <= to_int a1.length }
...
...
@@ -341,7 +305,7 @@ module Array63
to_int ofs2 <= i < to_int ofs2 + to_int len ->
a2[i] = a1[to_int ofs1 + i - to_int ofs2] }
val self_blit (a: array
~
'a) (ofs1: int63) (ofs2: int63) (len: int63) : unit
val self_blit (a: array 'a) (ofs1: int63) (ofs2: int63) (len: int63) : unit
writes {a}
requires { 0 <= to_int ofs1 /\ 0 <= to_int len /\
to_int ofs1 + to_int len <= to_int a.length }
...
...
theories/tptp.why
View file @
c13b1932
...
...
@@ -48,6 +48,7 @@ theory Rat
predicate (< ) (x y : rat)
predicate (> ) (x y : rat) = y < x
predicate (<=) (x y : rat) = x < y \/ x = y
predicate (>=) (x y : rat) = y <= x
clone export algebra.OrderedField
with type t = rat, predicate (<=) = (<=)
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment