ACSL-by-Example книга со спецификациями на frama-c всех стандартных алгоритмов (1184405), страница 19
Текст из файла (страница 19)
¬full(q) ∧ ¬empty(q) → pop(push(q, v)) = push(pop(q), v) for queues), thecontract length is not increased.1351234567891011121314/*@requires IsValidStack(s);requires !IsEmptyStack(s);assigns s->size;ensures IsValidStack(s);ensures \result == SizeOfStack{Old}(s) - 1;*/size_type axiom_size_of_pop(Stack* s){pop_stack(s);return size_stack(s);}Listing 8.40: Specification of Axiom (8.7)1234567891011121314/*@requires IsValidStack(s) && !IsEmptyStack(s);assigns s->size;assigns s->obj[s->size-1];ensures IsEqualStack{Here,Old}(s, s);/*void axiom_push_of_pop_top(Stack* s){const value_type val = top_stack(s);pop_stack(s);push_stack(s, val);}Listing 8.41: Specification of Axiom (8.9)1369. Results from Deductive VerificationIn this chapter we present to what extent the examples from Chapters 3 – 8 could be deductivelyverified using the Jessie plug-in of Frama-C and several automatic theorem provers.
For theseexperiments we used the Boron-20100401 release of Frama-C and the version 2.27 of the WhyPlatform.For each algorithm, the number of generated verification conditions are listed, as well as the percentage of proven verification conditions for each prover. All of the experiments were conductedon a Mac OS X running the Leopard operating system.Table 9.1 shows the four automatic theorem provers (ATP) used in conjunction with Jessie.Automatic Theorem ProverAlt-ErgoCVC3SimplifyZ3Version0.922.21.5.72.11Table 9.1.: Automatic theorem provers used during deductive verificationAlt-Ergo is an automatic theorem prover dedicated to program verification developed at Labora-toire de Recherche en Informatique (LRI) [19].
Alt-Ergo is freely available, under the termsof the CeCILL-C LICENSE.56CVC3 is an automatic theorem prover for Satisfiability Modulo Theories (SMT) problems [20].It was developed at New York University (NYU) and there is “essentially no limit on its usefor research or commercial purposes”.57Simplify is an automatic theorem prover [21]. The development of Simplify is not continued any-more. Nevertheless, it is still a highly efficient prover. As Chapter 9 demonstrates, Simplifyis the only prover that could verify all generated proof obligations from this tutorial.Z3 is a high-performance theorem prover developed at Microsoft Research [22]. A version fornon-commercial use is also available.5856For Details see http://alt-ergo.lri.fr/http/CeCILL-Cand http://en.wikipedia.org/wiki/CeCILL.57See http://www.cs.nyu.edu/acsys/cvc3/doc/LICENSE.html.58See http://research.microsoft.com/en-us/um/redmond/projects/z3/faq.html137Table 9.2 shows the results of the individual provers for the non-mutating algorithms (Chapter 3).For each algorithm there is at least one prover that is able to prove all verification conditions.Algorithmequalequal (mismatch)mismatchfindfind (reconsidered)find first ofadjacent findcountsearchSection3.13.23.23.33.43.53.63.73.8# VC20826242424332945Percentage of Proved VCsAlt-Ergo CVC3 SimplifyZ3100 % 100 %100 %95 %100 % 100 %62 % 100 %100 % 100 %100 %96 %100 % 100 %100 %96 %100 % 100 %100 %96 %100 % 100 %92 %96 %100 % 100 %100 %97 %100 %90 %100 %93 %93 % 100 %100 % 100 %Table 9.2.: Results for non-mutating algorithmsTable 9.3 contains the results for the maximum and minimum algorithms (Chapter 4).
In the firstrow we show that the < operator fulfills the properties of a partial order and we verify the semanticsof the derived operators. Again, all verification conditions of every algorithm are proven by at leastone of the provers.Algorithmpartial order properties of operator <max elementmax element (variant)max seqmin elementSection44.14.24.34.4# VC64242542Percentage of Proved VCsAlt-Ergo CVC3 SimplifyZ3100 % 100 %100 % 100 %100 % 100 %100 % 100 %100 % 100 %100 %95 %100 % 100 %100 % 100 %100 % 100 %100 % 100 %Table 9.3.: Results for maximum and minimum algorithms138Table 9.4 depicts the results for the binary search algorithms described in Chapter 5.
All verification conditions can be proved by at least one prover.Algorithmlower boundupper boundbinary searchSection5.15.25.3# VC34368Percentage of Proved VCsAlt-Ergo CVC3 SimplifyZ391 %94 %100 % 100 %91 %94 %100 % 100 %100 %88 %100 % 100 %Table 9.4.: Results for binary search algorithmsTable 9.5 contains the results for the mutating algorithms (Chapter 6). Note, that none of theprovers is able to prove each verification condition generated for rotate copy.
However, Simplify was able to prove each proof obligation except for the one describing arithmetic overflow.Algorithmfillswapswap valuesswap rangescopyreverse copyreverserotate copyreplace copyremove copyunique copyiotaSection6.16.26.36.46.56.66.66.76.86.96.106.11# VC157628202130932355420Percentage of Proved VCsAlt-Ergo CVC3 SimplifyZ3100 % 100 %100 %93 %100 % 100 %100 % 100 %83 %83 %100 % 100 %79 %86 %100 %86 %95 %95 %100 %95 %100 % 100 %100 %95 %83 %83 %100 %83 %78 %78 %89 %78 %88 %94 %100 %88 %94 %94 %100 %91 %91 %91 %100 %91 %95 % 100 %100 %95 %Table 9.5.: Results for mutating algorithms139Table 9.6 shows the results for the heap algorithms (Chapter 7). Some of the algorithms couldnot completely be proven by any automatic prover.
However, Simplify was able to prove eachverification condition except for the ones generated to examine arithmetic overflows in the “safety”group. This group of proof obligations was proven by Alt-Ergo, CVC3 or Yices instead.Algorithmis heappush heappop heapmake heapsort heapheap sortSection7.27.37.47.57.67.7# VC433611018226Percentage of Proved VCsAlt-Ergo CVC3 SimplifyZ391 %98 %100 %93 %92 %94 %92 %94 %95 %91 %96 %95 %100 % 100 %100 % 100 %95 %95 %95 %95 %100 % 100 %100 %83 %Table 9.6.: Results for heap algorithmsTable 9.7 shows the results for the stack functions described in Section 8.7. Each stack functionincludes the verification of the lemma introduced in Listing 8.11 to prove their well-definition.Regarding the well-definition, not all verification conditions can be proven by one prover.
Again,Simplify is able to verify each proof obligation except for the ones to examine arithmetic overflows. These proof obligations can be proven by Alt-Ergo, CVC3 or Yices instead.Algorithmequal stackreset stacksize stackempty stackfull stacktop stackpush stackpop stackrepresentation independenceSection8.68.7.18.7.28.7.38.7.48.7.58.7.68.7.78.7.1–8.7.7# VC1596131313312050Percentage of Proved VCsAlt-Ergo CVC3 SimplifyZ3100 % 100 %100 % 100 %100 % 100 %100 % 100 %100 % 100 %100 % 100 %100 % 100 %92 % 100 %100 % 100 %77 % 100 %100 % 100 %100 %92 %94 % 100 %100 % 100 %100 % 100 %100 %95 %96 %98 %92 %98 %Table 9.7.: Results for stack functions140In Table 9.8 the verification results for the stack axioms are depicted (Section 8.8).Algorithmaxiom size of resetaxiom size of pushaxiom top of pushaxiom pop of pushaxiom size of popaxiom push of pop topSection8.8.18.8.28.8.28.8.38.8.38.8.3# VC677867Percentage of Proved VCsAlt-Ergo CVC3 SimplifyZ3100 % 100 %100 % 100 %100 % 100 %100 % 100 %100 % 100 %100 % 100 %100 %88 %100 % 100 %100 % 100 %100 % 100 %100 %86 %100 % 100 %Table 9.8.: Results for stack axioms141A.
ChangesA.1. New in Version 5.1.1 (February 2011)• prepared algorithms for checking by the new WP plug-in of Frama-C• changed to Alt-Ergo Version 0.92, Z3 Version 2.11 and Why 2.27• added List of user-defined predicates and logic functions• added remarks on the relation of logical values in C and ACSL (see Section 1.3)• rewrote section on equal (Section 3.1) and mismatch (Section 3.2)• used a simpler logical function to count elements in an array (see Section 3.7)• added search algorithm (see Section 3.8)• added Chapter 4 to unite the maximum/minimum algorithms• added Chapter 5 for the new lower bound, upper bound and binary search algorithms• added swap values algorithm (see Section 6.3)• used IsEqual predicate for swap ranges (Section 6.4) and copy (Section 6.5)• added reverse copy and reverse algorithms (see Section 6.6)• added rotate copy algorithm (see Section 6.7)• added unique copy algorithm (see Section 6.10)• added Chapter 8 on specification of the data type StackA.2.
New in Version 5.1.0 (May 2010)• adaption to Frama-C Boron and Why 2.26 releases• changed from the -jessie-no-regions command-line option to using the pragmaSeparationPolicy(value)A.3. New in Version 4.2.2 (May 2010)• changed to latest version of CVC3 2.2143• added additional remarks to our implementation of find first of• changed size_type (int) to integer in all specifications• removed casts in fill and iota• renamed is_valid_range as IsValidRange• renamed has_value as HasValue• renamed predicate all_equal as IsEqual• extended timeout to 30 sec.A.4.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
