Difference between revisions of "C generic Team1 (E-ACSL) Benchmark3"
From CRV
(→Vampire number) |
(→Benchmark Data) |
||
| Line 10: | Line 10: | ||
==== Informal Description ==== | ==== 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 ==== | ==== Demonstration Traces ==== | ||
| Line 16: | Line 31: | ||
The formal property is given using the [http://frama-c.com/acsl.html ACSL] | The formal property is given using the [http://frama-c.com/acsl.html 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 | ||
| + | |||
| + | 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 ==== | ==== A FO-LTL Specification ==== | ||
Revision as of 17:07, 3 June 2016
Contents
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 property is given using the 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
fangs_t* vampire_fangs(uint64_t x)
and fangs_t is defined as:
struct fangs_t {
uint64_t fang1;
uint64_t fang2;
} ;
