11 Commits

Author SHA1 Message Date
Andrei Paskevich
3296edbb23 Dexpr: emit a warning for spurious olds in val contracts 2021-03-12 20:56:41 +01:00
Andrei Paskevich
3a9ea01ed9 Matrix: add the pure "update" function for applicative updates 2018-07-02 17:15:42 +02:00
Andrei Paskevich
eae547d95f stdlib, examples: remove redundant "import" 2018-06-15 16:45:58 +02:00
Andrei Paskevich
7b0929a761 WhyML: "use/clone T" imports by default (in absence of "as")
For the previous behaviour (no import), write "use/clone T as T".

This shortens the most used "use/clone import" to simply "use/clone".
2018-06-15 16:45:58 +02:00
Andrei Paskevich
9ea8a6a49c examples: add the missing proofs for type witnesses
Not done: double_wp/logic and avl/table.

The subgoal pairing changed in verifythis_2017_tree_buffer
in an unrelated VC (see the diff for why3session.xml). FIXME?
2017-06-26 00:01:12 +02:00
Guillaume Melquiond
d0c6f75ea7 Fix some examples with model types. 2016-03-23 17:20:20 +01:00
Claude Marche
a5e8979774 New post for Array.make, updated examples that need Const.const 2015-07-06 14:02:05 +02:00
Jean-Christophe Filliatre
9bd9044694 new example bag (uses null.Null) 2014-11-21 15:13:35 +01:00
Jean-Christophe Filliatre
8de522be6c gallery: a spec module for resizable_array 2014-01-27 14:14:28 +01:00
Jean-Christophe
f09f05cbb6 resizable_array: make it polymorphic, additional invariant 2013-03-04 13:04:37 +01:00
Andrei Paskevich
4b1bc2b0c0 reorganize examples/
- all programs with sessions are in examples/
- all programs without sessions are in examples/in_progress/
  (if you have private sessions for those, just move them there)
- all pure logical problems are in logic/
  (to simplify bench scripts and gallery building; they are few anyway)
- all OCaml programs are in examples/use_api/
- all strange stuff is in examples/misc/
  (most of it should probably go)
- Claude's solutions for Foveoos 2011 are in examples/foveoos11-cm/
  (why do we need two sets of solutions for quite simple problems?)
- hoare_logic, bitvectors, vacid_0_binary_heaps are in examples/

Bench scripts and documentation are updated.
Also, bench/bench is simplified a little bit.
2013-01-30 01:23:44 +01:00