programs: more libraries

parent bd7a731b
......@@ -42,8 +42,6 @@ module Array
(forall i:int. 0 <= i < length a1 -> result[i] = a1[i]) and
(forall i:int. 0 <= i < length a2 -> result[length a1 + i] = a2[i]) }
(* concat : 'a array list -> 'a array *)
parameter sub : a:array 'a -> ofs:int -> len:int ->
{ 0 <= ofs and ofs + len <= length a }
array 'a
......@@ -61,13 +59,28 @@ module Array
unit
writes a
{ (forall i:int.
(0 <= i < ofs or ofs + len <= i < length a) -> a[i] = (old a)[i]) and
(0 <= i < ofs or ofs + len <= i < length a) -> a[i] = (old a)[i])
and
(forall i:int.
ofs <= i < ofs + len -> a[i] = v) }
(* blit : 'a array -> int -> 'a array -> int -> int -> unit *)
parameter blit :
a1:array 'a -> ofs1:int -> a2:array 'a -> ofs2:int -> len:int ->
{ 0 <= ofs1 and ofs1 + len <= length a1 and
0 <= ofs2 and ofs2 + len <= length a2 }
unit
writes a2
{ (forall i:int.
(0 <= i < ofs2 or ofs2 + len <= i < length a2) -> a2[i] = (old a2)[i])
and
(forall i:int.
ofs2 <= i < ofs2 + len -> a2[i] = a1[ofs1 + i - ofs2]) }
(* to_list / of_list *)
(* TODO?
- concat : 'a array list -> 'a array
- to_list
- of_list
*)
end
......@@ -76,7 +89,7 @@ module TestArray
use import int.Int
use import module Array
let test1 () =
let test_append () =
let a1 = make 17 2 in
assert { a1[3] = 2 };
a1[3 <- 4];
......@@ -89,15 +102,25 @@ module TestArray
assert { a[17] = 3 };
()
let test2 () =
let test_fill () =
let a = make 17 True in
fill a 10 4 False;
assert { a[10] = False }
let test_blit () =
let a1 = make 17 True in
let a2 = make 25 False in
blit a1 10 a2 17 7;
assert { a1[10] = True };
assert { a2[16] = False };
assert { a2[17] = True };
assert { a2[23] = True };
assert { a2[24] = False }
end
(*
Local Variables:
compile-command: "unset LANG; make -C .."
compile-command: "unset LANG; make -C .. modules/stdlib"
End:
*)
......@@ -9,6 +9,26 @@ module Char
parameter code : c:char -> {} int { result = c and 0 <= c <= 255 }
logic uppercase int : int
logic lowercase int : int
axiom uppercase_alpha:
forall c:int. 97 <= c <= 122 -> uppercase c = c - 32
axiom uppercase_other:
forall c:int. 0 <= c < 97 or 122 < c <= 127 -> uppercase c = c
axiom lowercase_alpha:
forall c:int. 65 <= c <= 90 -> lowercase c = c + 32
axiom lowercase_other:
forall c:int. 0 <= c < 65 or 90 < c <= 127 -> lowercase c = c
parameter uppercase : c:char -> {} char { result = uppercase c }
parameter lowercase : c:char -> {} char { result = lowercase c }
(* TODO
- compare ?
*)
end
module String
......@@ -21,6 +41,12 @@ module String
parameter create : len:int -> { len >= 0 } string { S.length result = len }
parameter make : len:int -> c:char ->
{ len >= 0 }
string
{ S.length result = len and
forall i:int. 0 <= i < len -> S.get result i = c }
parameter get : s:string -> i:int ->
{ 0 <= i < S.length s } char reads s { result = S.get s i }
......@@ -29,6 +55,37 @@ module String
parameter length : s:string -> {} int reads s { result = S.length s }
parameter copy : s:string ->
{}
string
{ S.length result = S.length s and
forall i:int. 0 <= i < S.length result -> S.get result i = S.get s i }
parameter uppercase : s:string ->
{}
string
{ S.length result = S.length s and
forall i:int. 0 <= i < S.length result ->
S.get result i = Char.uppercase (S.get s i) }
parameter lowercase : s:string ->
{}
string
{ S.length result = S.length s and
forall i:int. 0 <= i < S.length result ->
S.get result i = Char.lowercase (S.get s i) }
(* TODO
- copy
- sub
- fill
- blit
- concat
- index / rindex / index_from / rindex_from
- contains / contains_from / rcontains_from
- capitalize / uncapitalize
*)
end
module Buffer
......@@ -60,21 +117,35 @@ module Buffer
S.sub b 0 (old (S.length b)) = old b and
S.sub b (old (S.length b)) (S.length s) = s }
(* TODO
- add_substring
- add_buffer
*)
end
module Test
use module Char
use module String
use array.ArrayRich as S
use module Buffer
let test () =
let test1 () =
let b = Buffer.create 1024 in
let c = Char.chr 65 in
Buffer.add_char b c;
let s = String.create 100 in
Buffer.add_string b s;
assert { String.S.length b = 101 }
assert { S.length b = 101 }
let test2 () =
let s = String.make 100 (Char.chr 65) in
assert { S.get s 42 = 65 }; (* 'A' *)
let c = Char.lowercase (String.get s 42) in
assert { c = 97 }; (* 'a' *)
let u = String.lowercase s in
assert { S.get u 41 = 97 }
end
......
......@@ -10,3 +10,19 @@ o fixed precedence of label (label L: e) wrt sequence (e ; e)
o model types (abstract but not mutable)
abstract types (no model)
o program alias, e.g.
let f = String.create
o library
x Array
- String
- Buffer
- Char
- Hashtbl
- Queue
- Stack
- List
- Map
- Set
\ No newline at end of file
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