Starting from the type definitions in http://www.cas.mcmaster.ca/~kahl/CAS707/2019/List.ltx,
specify and implement the two append functions discussed in class.
Specification-level lists are shown in the ACSL definition in Example 2.41 (p. 52). (Section 2.68 (pp. 54–55) describes concrete logic types, which, according to Fig. 2.17 are not yet implemented in Frama-C.)
Section 2.7.2 (p. 60) introduces \separated (in the grammar Fig. 2.20 on p. 59) — understand the specification on p. 60!
This points to section 2.3.4 (p. 35) for “tsets”.
Define a predicate separatedLists{L}(list xs, list ys) that captures separation of the
memory occupied by xs and ys.
Document your explorations again in LaTeX using listingsACSL.sty.
(The home of ACSL By Example is https://github.com/fraunhoferfokus/acsl-by-example;
we looked at equal from section 3.5.)