CHANGES

Library ENUM

Version 1.0
===========

- C generators, specified in ACSL for verification with the WP plugin of the 
  Frama-C platform

- Downloadable at http://members.femto-st.fr/alain-giorgetti/en

Version 1.1
===========

+ Folder Why3 with some WhyML generators, for verification with Why3

Version 1.2
===========

+ Folder cACSL with a significant part of ENUM 1.0

o Folder Why3 with more WhyML generators than in ENUM 1.1

+ Installation with Docker

+ Dockerfile

Version 1.3
===========

+ New file INSTALL.md

+ New documentation docs/EG19.pdf

o Updated Dockerfile, with more recent tool versions and vim to edit files

o Simpler code for small_check in Why3/generator/lexgen.mlw

+ New generator in Why3/generator/blist/ for bounded lists

- The docker container creation script ctrmac.sh for Mac OS no longer works

- Soundness and completeness proofs for ptrWhy3/permutation/Permutation.mlw
  are temporarily broken. They will be restored in a subsequent release.