release 32.0.1

Author: jensgerlach

ACSL-by-Example.pdf

@@ -7,54 +7,26 @@ provided in `README.md`.
 
 ---
 
-## Version 32.0.0  
+## Version 32.0.1  
 (Targeting Frama-C 32.0 “Germanium”)
 
 ### Improvements
 
-- **Adaptation to Frama-C/WP evolution**  
-  The specifications and accompanying Coq proofs have been revised to reflect
-  changes in the WP plugin and its generated proof obligations.
+- Added `terminates` and `exits` clauses to all function contracts.
 
-- **Renamed and clarified logical concepts**  
-  The logic predicate `RemovePartition` has been renamed to
-  `IndexOfNotEqual`.  The corresponding specifications, implementations
-  (`remove`, `remove_copy3`), and tutorial text have been updated accordingly.
+- Completed the `assigns` clauses of `stackinit` and `axiomsizeofinit`
+  with explicit `\from` dependencies, clarifying the origin of assigned
+  values and aligning the contracts with WP’s pedantic assigns checks.
 
-- **Additional supporting lemmas**  
-  New lemmas have been introduced to improve proof automation and robustness,
-  in particular:
-  - `AccumulateNext`
-  - `InnerProductInit`
-  - `InnerProductNext`
+- Replaced statement contracts in `pop_heap`, `partial_sort`,
+  `selection_sort`, `insertion_sort`, and `merge` by assertions referring to
+  an explicit ghost label, thereby making the proof obligations local to
+  the respective loop bodies.
 
-- **Tutorial cleanup**  
-  Obsolete references to `count2` have been removed from the report.
+- Improved the description of non-mutating algorithms; removed `count2`
+  and the inductively defined logic function `CountInd`.
 
-- **Build system fixes**  
-  Minor corrections and cleanups have been applied to the Makefiles to ensure
-  consistent verification runs with the current toolchain.
-
----
-
-### Open issues
-
-The following issues are known and mainly stem from changes in the behavior or
-diagnostics of Frama-C/WP.  They do not affect the correctness of the examples
-but may result in warnings during verification.
-
-- **Missing explicit `terminates` / `exits` clauses**  
-  Some function contracts omit explicit `terminates` and/or `exits` clauses.
-  WP therefore inserts default clauses, which may lead to warnings.
-
-- **Pedantic assigns warnings**  
-  In a few cases, WP reports `wp:pedantic-assigns` warnings where the `assigns`
-  clause is missing or weaker than the implementation.
-
-- **Ignored statement-level specifications**  
-  Certain statement contracts are currently ignored by WP and trigger
-  informational warnings.
-
-These issues are expected to be addressed in future revisions of
-*ACSL by Example*.
+- Improved the description of minimum and maximum algorithms.
 
+- Improved the description of binary search algorithms and removed
+  `binary_search2`.

CHANGES.md

@@ -1,6 +1,6 @@
 MIT License
 
-Copyright (c) 2020 Jens Gerlach
+Copyright (c) 2020-2026 Fraunhofer FOKUS
 
 Permission is hereby granted, free of charge, to any person obtaining a copy
 of this software and associated documentation files (the "Software"), to deal
@@ -19,3 +19,4 @@ AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
 OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
 SOFTWARE.
+

LICENSE.md

@@ -1,7 +1,7 @@
 
 # ACSL by Example
 
-This repository contains version 32.0.0 of
+This repository contains version 32.0.1 of
 [ACSL by Example](https://github.com/fraunhoferfokus/acsl-by-example/blob/master/ACSL-by-Example.pdf)
 --- a curated collection of C functions and data types whose behavior has been
 formally specified using **ACSL** (ANSI/ISO C Specification Language) and

README.md

@@ -2,7 +2,7 @@
 #ifndef ARRAYBOUNDS_ACSL_INCLUDED
 #define ARRAYBOUNDS_ACSL_INCLUDED
 
-#include "typedefs.h"
+#include "LessThanComparable.acsl"
 
 /*@
   axiomatic ArrayBounds

StandardAlgorithms/Logic/ArrayBounds.acsl

@@ -57,13 +57,6 @@
         m <= k <= n  ==>
         Find(a, m, k, v) <= Find(a, m, n, v);
 
-    lemma Find_Extend:
-      \forall value_type *a, v, integer k, m, n;
-        m <= k < n                ==>
-        a[k] == v                 ==>
-        Find(a, m, k, v) == k-m   ==>
-        Find(a, m, n, v) == k-m;
-
     lemma Find_Limit:
       \forall value_type *a, v, integer k, m, n;
         m <= k < n  ==>