Difference between revisions of "C generic Team1 (E-ACSL) Benchmark2"
(→Loop invariant) |
(→Benchmark Data) |
||
| Line 8: | Line 8: | ||
=== The Property Part === | === The Property Part === | ||
| + | |||
| + | Given a loop that iterates over all elements of an integer array '''A''' starting with an element at position 0 and compares each element to some number '''N''' the following loop invariant holds: | ||
| + | A[i] < N, | ||
| + | where '''i''' denotes an index in an array during the iteration. | ||
==== Informal Description ==== | ==== Informal Description ==== | ||
| + | |||
| + | This benchmark aims to explore validating loop invariants. The following benchmark implements a simple version of a linear search that uses a loop to iterate over the elements of the sorted array of integers and identify whether a given number exists in this array. The aim of the benchmark is to identify whether the following property holds at runtime. | ||
==== Demonstration Traces ==== | ==== Demonstration Traces ==== | ||
| Line 16: | Line 22: | ||
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] | ||
| + | |||
| + | /*@ loop invariant \forall integer i; 0 <= i < k ==> array[i] < elt; */ | ||
| + | |||
| + | where '''array''' is of integer array type and '''k''' and '''elt''' are of integral types. | ||
==== A FO-LTL Specification ==== | ==== A FO-LTL Specification ==== | ||
Revision as of 17:00, 3 June 2016
Contents
Benchmark Data
This benchmark is located in crv.liflab.ca@/home/e-acsl/crv16_benchmarks/c-generic-track/loop-invariant
The Trace Part
E-ACSL has no notion of trace
The Property Part
Given a loop that iterates over all elements of an integer array A starting with an element at position 0 and compares each element to some number N the following loop invariant holds:
A[i] < N,
where i denotes an index in an array during the iteration.
Informal Description
This benchmark aims to explore validating loop invariants. The following benchmark implements a simple version of a linear search that uses a loop to iterate over the elements of the sorted array of integers and identify whether a given number exists in this array. The aim of the benchmark is to identify whether the following property holds at runtime.
Demonstration Traces
Formal Specification
The formal property is given using the ACSL
/*@ loop invariant \forall integer i; 0 <= i < k ==> array[i] < elt; */
where array is of integer array type and k and elt are of integral types.
