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

Latest revision as of 10:06, 5 June 2016

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.

A FO-LTL Specification