CAS 707 ─ Formal Specification Techniques ─ Winter 2018
Assignment 4
Please log your experiments in a document as usual; for pretty-printing of ACSL and ACSL-annotated C-code, use listingsACSL.sty (improvements welcome!) in the following way:
\usepackage{listings} \usepackage{listingsACSL} ... \lstset{language=[ACSL]C,...}
4.1 Read Allan Blanchard's tutorial
Go at least over Chapters 1–5.
4.2 Read ACSL by Example Chapters 1–3
Can you re-write the implementation of find
(Listing 3.3)
so that only a single return
occurs at the end of the procedure,
using a while
loop without break
or continue
or goto
?
(For that shape, you could actually produce a Hoare logic proof using
the rules you know.)
Do you need to change also the annotation for the
verification of the implementation to go through?
Can you unify the specification of find_first_of
(Listing 3.9)
so that it does not need =behavior=s anymore?
Does the verification of the implementation still go through?
In Listing 3.15, can you express also the second version of
EqualRanges
in terms of the first?
What is the “standard” algorithm for the problem of search
(Section 3.6)?
(Solution linked here.)
The Wikipedia page with the solution also has a link to “C code”;
how far can you get towards verification of that code against the
(possibly adapted) search
specification? (Open-ended bonus
question, collaboration allowed, no deadline.)
Can you re-write the implementation of search_n
(Listing 3.28)
so that only a single return
occurs at the end of the procedure,
using a while
loop without break
or continue
or goto
?
Do you need to change also the annotation for the
verification of the implementation to go through?