Difference between revisions of "C generic Team1 (E-ACSL) Benchmark3"

From CRV
Jump to: navigation, search
(Formal Specification)
(Formal Specification)
Line 42: Line 42:
 
   @ ensures  \valid(\result) ==> !(\result->fang1%10 == 0 && \result->fang2%10 == 0); */
 
   @ ensures  \valid(\result) ==> !(\result->fang1%10 == 0 && \result->fang2%10 == 0); */
  
Where the above is a contract for a function
+
where the above is a contract for a function with the following signature.
  
 
  fangs_t* vampire_fangs(uint64_t x)
 
  fangs_t* vampire_fangs(uint64_t x)

Revision as of 10:08, 5 June 2016

Benchmark Data

This benchmark is located in crv.liflab.ca@/home/e-acsl/crv16_benchmarks/c-implicit-track/vampire-number

The Trace Part

E-ACSL has no notion of trace

The Property Part

Informal Description

Check a property related to correct computation of a vampire number.

A vampire number V is a natural number with an even number of digits that can be factored into two integers (fangs) with the following properties:

  • Each fang F of a vampire number V contains exactly D/2 digits, where D is a number of digits of V.
  • A pair of fangs (F1, F2) of a vampire number V are composed of the same digits as V itself.
  • Given a pair of the fangs (F1, F2) of a vampire number V, F1 and F2 do not contain trailing zeroes, i.e.,
F1%10 + F2%10 > 0,

where % is a modulo operator.

Vampire number examples:

1260 = 21 x 60
104260 = 260 x 401
13078260 = 1620 × 8073

Demonstration Traces

Formal Specification

The formal specification is given using ACSL

/*@ ensures  \valid(\result) <==> \result != \null;
 @ ensures  \valid(\result) ==> \result->fang1 != 0;
 @ ensures  \valid(\result) ==> \result->fang2 != 0;
 @ ensures  \valid(\result) ==> ndigits(\result->fang1) == ndigits(x)/2;
 @ ensures  \valid(\result) ==> ndigits(\result->fang2) == ndigits(x)/2;
 @ ensures  \valid(\result) ==> ndigits(x)%2 == 0;
 @ ensures  \valid(\result) ==> \result->fang2*\result->fang1 == x;
 @ ensures  \valid(\result) ==> !(\result->fang1%10 == 0 && \result->fang2%10 == 0); */

where the above is a contract for a function with the following signature.

fangs_t* vampire_fangs(uint64_t x)

and fangs_t is defined as:

struct fangs_t {
  uint64_t fang1;
  uint64_t fang2;
} ;

A FO-LTL Specification