--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on March 2020 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] ACSL by Example (version 20.0.1)



Dear Frama-C users,

Fraunhofer FOKUS has just released a new version (20.0.1) of “ACSL by Example”.
This version is intended for Frama-C/WP 20.0.
The examples can be accessed through Github

        https://github.com/fraunhoferfokus/acsl-by-example

The PDF document can be directly accessed through

        https://github.com/fraunhoferfokus/acsl-by-example/blob/master/ACSL-by-Example.pdf

Here are the most important changes

	- Improve specification of remove_copy and remove by providing an explicit definition of 
          of the logic function RemovePartition. This allows to replacing the axioms by lemmas.
	- Improve text and layout in many places
	- Make names of ACSL predicates, functions and lemmas more uniform and place them
          together in files where appropriate

Please refer to the changes section for a more detailed description.

We hope that this version helps you in learning and applying Frama-C/WP!

Jens Gerlach