C generic Team1 (E-ACSL) Benchmark2
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.
