Difference between revisions of "C generic Team1 (E-ACSL) Benchmark2"
(→Benchmark Data) |
(→Formal Specification) |
||
| (One intermediate revision by the same user not shown) | |||
| Line 21: | Line 21: | ||
==== Formal Specification ==== | ==== Formal Specification ==== | ||
| − | The formal | + | The formal specification is given using [http://frama-c.com/acsl.html ACSL] |
/*@ loop invariant \forall integer i; 0 <= i < k ==> array[i] < elt; */ | /*@ loop invariant \forall integer i; 0 <= i < k ==> array[i] < elt; */ | ||
Latest revision as of 10:06, 5 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 specification is given using 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.
