Guillaume Melquiond
|
46d53c02a9
|
Mark some types as having an extensional equality.
|
2024-11-13 19:04:52 +01:00 |
|
Guillaume Melquiond
|
09a71c74c0
|
Fix occurrences of "occurences".
|
2023-11-23 19:04:11 +01:00 |
|
MARCHE Claude
|
bcfef9818c
|
Resolve "Fix drivers for SMT-LIB strings"
|
2022-04-06 14:29:41 +00:00 |
|
Guillaume Melquiond
|
ea123b5e95
|
Improve documentation of standard library.
|
2021-09-21 18:00:14 +02:00 |
|
Jean-Christophe Filliatre
|
7586ce70d8
|
stdlib: fixed string.OCaml.([])
was missing a precondition because the contract was written *after*
the function body, not before
|
2020-07-14 15:41:56 +02:00 |
|
Jean-Christophe Filliatre
|
82c2eb65f1
|
a better way to provide that the length of string is nonnegative
|
2020-06-19 14:04:36 +02:00 |
|
Jean-Christophe Filliatre
|
c9de030b18
|
improved session of string_search with a lemma
|
2020-06-19 12:28:13 +02:00 |
|
Cláudio Belo Lourenço
|
5ad0e3fcb8
|
String stdlib documentation
|
2020-03-04 15:42:24 +01:00 |
|
Jean-Christophe Filliatre
|
9e033eaa77
|
strings: make OCaml.length a partial function
|
2020-02-21 10:33:52 +01:00 |
|
Jean-Christophe Filliatre
|
b13bca590c
|
updated proof sessions using strings
|
2020-02-20 15:28:46 +01:00 |
|
Jean-Christophe Filliatre
|
97247b2a68
|
string_base64_encoding: cleaning up
|
2020-02-20 14:57:01 +01:00 |
|
Jean-Christophe Filliatre
|
5f3098b962
|
OCaml strings are now an abstract data type
this is to ensure that OCaml strings have a length no greater than
max_int; actually, no greater than max_string_length, which is smaller
|
2020-02-20 14:46:09 +01:00 |
|
Jean-Christophe Filliatre
|
69dd070343
|
make string.Char.char an abstract type
|
2020-02-20 14:08:41 +01:00 |
|
Jean-Christophe Filliatre
|
a3b5386d51
|
new library string.StringBuffer
this is extracted to OCaml's Buffer
|
2020-02-20 11:37:29 +01:00 |
|
Cláudio Belo Lourenço
|
ba06e713d3
|
eq_char for char equality
|
2020-02-17 14:55:53 +01:00 |
|
Cláudio Belo Lourenço
|
d5cb482a25
|
Moving provable lemmas into string theory as axioms
|
2020-02-12 16:08:42 +01:00 |
|
Jean-Christophe Filliatre
|
ecfc319521
|
removed a warning in string.String
|
2020-02-12 13:40:19 +01:00 |
|
Jean-Christophe Filliatre
|
e82458d596
|
string.String: relaxed preconditions on two axioms
|
2020-02-12 13:32:40 +01:00 |
|
Cláudio Belo Lourenço
|
89799ff159
|
Base64 encoding and decoding proofs
|
2020-01-24 15:43:50 +01:00 |
|
Cláudio Belo Lourenço
|
958be1002b
|
Base64 enccode - proof completed.
|
2020-01-24 15:43:50 +01:00 |
|
Cláudio Belo Lourenço
|
0d13699eab
|
Encoding Base64 proof (wip)
|
2020-01-24 15:43:50 +01:00 |
|
Cláudio Belo Lourenço
|
ba8a674a1e
|
Proof of hexadecimal encoding (wip)
|
2020-01-24 15:43:50 +01:00 |
|
Cláudio Belo Lourenço
|
2b4d6078b2
|
String theory: change [] to s_at (at is a why3 reserved keyword)
|
2020-01-24 15:43:50 +01:00 |
|
Cláudio Belo Lourenço
|
468487642b
|
String theory improvements
|
2020-01-24 15:43:50 +01:00 |
|
Cláudio Belo Lourenço
|
f1dd51f8aa
|
Organization of program functions in string theory
|
2020-01-24 15:43:50 +01:00 |
|