Commit 19cb2ee1 authored by MARCHE Claude's avatar MARCHE Claude

modules mach.array.*: add explanations

parent 8a6206c0
...@@ -24,11 +24,11 @@ module Array32 ...@@ -24,11 +24,11 @@ module Array32
function ([<-]) (a: array 'a) (i: int) (v: 'a) : array 'a = set a i v function ([<-]) (a: array 'a) (i: int) (v: 'a) : array 'a = set a i v
val ([]) (a: array ~'a) (i: int32) : 'a val ([]) (a: array ~'a) (i: int32) : 'a
requires { 0 <= to_int i < to_int a.length } requires { "expl:index in array bounds" 0 <= to_int i < to_int a.length }
ensures { result = a[to_int i] } 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 { 0 <= to_int i < to_int a.length } 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 } ensures { a.elts = M.set (old a.elts) (to_int i) v }
val length (a: array ~'a) : int32 ensures { result = a.length } val length (a: array ~'a) : int32 ensures { result = a.length }
...@@ -54,7 +54,7 @@ module Array32 ...@@ -54,7 +54,7 @@ module Array32
{ length = n; elts = M.const v } { length = n; elts = M.const v }
val make (n: int32) (v: ~'a) : array 'a val make (n: int32) (v: ~'a) : array 'a
requires { to_int n >= 0 } requires { "expl:array creation size" to_int n >= 0 }
ensures { result = make n v } ensures { result = make n v }
val append (a1: array ~'a) (a2: array 'a) : array 'a val append (a1: array ~'a) (a2: array 'a) : array 'a
...@@ -141,11 +141,11 @@ module Array31 ...@@ -141,11 +141,11 @@ module Array31
function ([<-]) (a: array 'a) (i: int) (v: 'a) : array 'a = set a i v function ([<-]) (a: array 'a) (i: int) (v: 'a) : array 'a = set a i v
val ([]) (a: array ~'a) (i: int31) : 'a val ([]) (a: array ~'a) (i: int31) : 'a
requires { 0 <= to_int i < to_int a.length } requires { "expl:index in array bounds" 0 <= to_int i < to_int a.length }
ensures { result = a[to_int i] } 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 { 0 <= to_int i < to_int a.length } 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 } ensures { a.elts = M.set (old a.elts) (to_int i) v }
val length (a: array ~'a) : int31 ensures { result = a.length } val length (a: array ~'a) : int31 ensures { result = a.length }
...@@ -171,7 +171,7 @@ module Array31 ...@@ -171,7 +171,7 @@ module Array31
{ length = n; elts = M.const v } { length = n; elts = M.const v }
val make (n: int31) (v: ~'a) : array 'a val make (n: int31) (v: ~'a) : array 'a
requires { to_int n >= 0 } requires { "expl:array creation size" to_int n >= 0 }
ensures { result = make n v } ensures { result = make n v }
val append (a1: array ~'a) (a2: array 'a) : array 'a val append (a1: array ~'a) (a2: array 'a) : array 'a
...@@ -258,11 +258,11 @@ module Array63 ...@@ -258,11 +258,11 @@ module Array63
function ([<-]) (a: array 'a) (i: int) (v: 'a) : array 'a = set a i v function ([<-]) (a: array 'a) (i: int) (v: 'a) : array 'a = set a i v
val ([]) (a: array ~'a) (i: int63) : 'a val ([]) (a: array ~'a) (i: int63) : 'a
requires { 0 <= to_int i < to_int a.length } requires { "expl:index in array bounds" 0 <= to_int i < to_int a.length }
ensures { result = a[to_int i] } 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 { 0 <= to_int i < to_int a.length } 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 } ensures { a.elts = M.set (old a.elts) (to_int i) v }
val length (a: array ~'a) : int63 ensures { result = a.length } val length (a: array ~'a) : int63 ensures { result = a.length }
...@@ -288,7 +288,7 @@ module Array63 ...@@ -288,7 +288,7 @@ module Array63
{ length = n; elts = M.const v } { length = n; elts = M.const v }
val make (n: int63) (v: ~'a) : array 'a val make (n: int63) (v: ~'a) : array 'a
requires { to_int n >= 0 } requires { "expl:array creation size" to_int n >= 0 }
ensures { result = make n v } ensures { result = make n v }
val append (a1: array ~'a) (a2: array 'a) : array 'a val append (a1: array ~'a) (a2: array 'a) : array 'a
......
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