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?