BlockLibrary instance verification

In this page we will describe the various techniques used in order to verify a BlockLibrary instance.

Purpose and goal to achieve

Here we would like to specify a generic algorithm for the completeness and soundness verification of the specification through the verification of the features (input ports, parameters,memories) data type definition domain and usage. The main idea is to verify:

  • For every feature, every possible value is handled in its definition domain (completeness).
  • Each signature of each BlockMode is different (uniqueness).
  • Each mode signature specify a distinct part of the block specification (disjointness).

Definition domain of a feature

A StruturalFeature is declared in a BlockVariant. Its data type is declared in the data types declaration at the root of the BlockLibrary.

For a StructuralFeature \(f\) declared in the BlockVariant \(v_1\), the definition domain of the feature is the set of BlockVariants extending \(v_1\) (and recursively all the extending BlockVariants) and the set of BlockModes implementing all the previous BlockVariants. Starting from a feature declaration, we consider a sub-tree \(ST\) of the specification tree for which the root is the BlockVariant in which the feature is declared.

Verification of the specification

We distinguish between three verification on a BlockLibrary instance:

  • Structural correctness of the specification. According to the structural specification (Ecore MM), is the block instance specification an instance of this metamodel ?
  • Variability specification correctness. Our language is based on Feature modeling principles, we want to check if the variable structures specified in the block instance specification is correct and sound ?
  • Semantics specification correctness. From the variable form of the specification, it is possible to extract the possible specifications for any block instance. We need to ensure the correctness of these semantics specifications.

Structural verification

Structural verification of a BlockLibrary is done with a set of OCL constraints. These constraints are described in the BlockLibrary Editors page and in the corresponding OCL file. Model driven engineering techniques provides a set of techniques for automatic verification of such properties. We choose to implement one on our textual editor in order to check all these OCL constraints during typing of the specification.

Variability correctness of the BlockLibrary

We gave in the Mode resolution page, some definitions for BlockMode and BlockVariant signatures.

BlockLibrary axiomatisation

We developed an axiomatisation of the BlockLibrary element. This allows us to define fundations for the formal specification and verification of any BlockLibrary instance. Each BlockLibrary element has been formalised in the Block library datatypes theories expressed using the why3 language. Basic scalar dataypes (double, int, boolean, ...) are already defined in Why3, we additionnaly defined some other basic datatypes based on the standard library specification (UINT8/16/32/64, INT8/16/32/64,...). Finally we need to have a String datatype, so we defined a theory for characters and strings.

We provide the full generated documentation for these elements.

BlockLibrary annotation languages formalisation

Annotations languages used in the BlockLibrary instance in order to specify the various constraints to be verified on the block instances are translated to their Why3 equivalent. In order to do so we rely on a formalisation of some of the OCL language constructs. Most interestingly, we formalised the first order logic operations on the manipulation of OCL collections (indexOf, at, ...) and the higher order logic operation on the filtering and application of operations on collections (collect, select, ...). These theories are described in the OCL specification theory. A translation from OCL expressions to Why3 has been developed.

BlockType signature

If we analyse a BlockType (\(t\)) specification, we get thanks to the BlockMode signature calculus a set of signatures for each BlockMode. We define the full specification of a BlockType (\(SPEC(t)\)) with:

\[\forall t : BlockType, \forall m \in t.modes, SPEC(t) = \{SIG(m_i)\}\]

We assume that \(t.modes\) is the set of modes contained in the BlockType \(t\).

Completeness of the specification

Checking for the completeness of a specification is providing the proof that this specification holds all the possible configurations for the content of the specification. In our case, we want to check that each BlockType signature is complete according to its included BlockModes.

So we would like to check that for any instance of a Block (\(b\)), there is a BlockMode signature (\(SIG(m_i)\)) for which, \(SIG(m_i)\) is a specification for \(b\).

Formal definition of this property is:

\[\bigvee^{n}_{i=1} SIG(m_i) = \top\]

Disjointness of the set of all specifications

We must also check for the disjointness of all the possible specifications etracted from a BlockType. Checking this is about proving that the set of all signatures is disjoint.

Formal definition of this property is:

\[\bigoplus^{n}_{i=1} SIG(m_i) = \top\]

Combination of completeness and disjointness

With the two previous results we are able to answer the question: does every possible combination of features handled exactly once in the block specification.

In other words does the signatures of all the possible combination of features (all the signatures of all the BLockModes in one BlockType) forms a partition of the specification of a BlockType.

This is the definition of the correctness of the specification.

Example of correctness verification

In this section we will detail the BlockLibrary verification process. In order to tackle this in the more practical way, we will use the example of the Lookup block specification. This block is the one dimensional version of the nD Lookup block from Simulink. The original documentation of the nD Lookup block is provided at Lookup block spec

Input: a blocklibrary instance

The specification for the Lookup block is provided here. Details about the textual representation for the BlockLibrary models is provided on the BlockLibrary Editors page.

library Simulink_Basic {
	type realDouble TDouble
	type realInt TRealInteger of 8 bits
	type enum LookupMethodEnum {InterpolationExtrapolation, InterpolationUseEndValues}
	
	type array InputValuesType of TDouble [20]
	type array TableType of TDouble [20]
	
blocktype Lookup {

		variant Lookup_Root isDynamic {
			out data S1 : TDouble
			in data E1 : TDouble
			parameter InputValues : InputValuesType {
				invariant ocl inputValuesOrdered {
					InputValues.value->forAll(e| 
						e <> InputValues.value->last() implies 
						e <= InputValues.value->at(
								InputValues.value->indexOf(e) + 1
						)
					)
				}
				invariant ocl {
					InputValues.value->size() = Table.value->size()
				}
				invariant ocl {
					InputValues.value->at(0) < InputValues.value->at(InputValues.value->size() - 1)
				}
				invariant ocl {
					InputValues.value->size() > 0
				}
			}
			parameter Table : TableType
			parameter LookupMethod : LookupMethodEnum
		}
		
		variant Lookup_InterpolationExtrapolation extends Lookup_Root {
			modeinvariant ocl {
				LookupMethod.value = !! LookupMethodEnum::InterpolationExtrapolation
			}
		}
 		mode Lookup_InterpolationExtrapolation_below implements Lookup_InterpolationExtrapolation {
 			modeinvariant ocl {
 				E1.value <= InputValues.value->at(0)
 			}
 			definition eml = compute_Lookup_InterpolationExtrapolation_below {
 				postcondition eml post_Lookup_InterpolationExtrapolation_below_final {
					S1.value == Table.value[0] + ((E1.value - InputValues.value[0]) * ((Table.value[1] - Table.value[0]) / (InputValues.value[1] - InputValues.value[0])));
				}
 				S1.value = Table.value[0] + ((E1.value - InputValues.value[0]) * ((Table.value[1] - Table.value[0]) / (InputValues.value[1] - InputValues.value[0])));
 			}
 			compute compute_Lookup_InterpolationExtrapolation_below
 		}
 		mode Lookup_InterpolationExtrapolation_above implements Lookup_InterpolationExtrapolation {
 			modeinvariant ocl {
 				E1.value >= InputValues.value->at(InputValues.value->size() - 1)
 			}
 			definition eml = compute_Lookup_InterpolationExtrapolation_above {
 				postcondition eml post_Lookup_InterpolationExtrapolation_above_final {
					S1.value == Table.value[size(Table.value) - 2] + ((E1.value - InputValues.value[size(Table.value) - 2]) * ((Table.value[size(Table.value) - 1] - Table.value[size(Table.value) - 2]) / (InputValues.value[size(Table.value) - 1] - InputValues.value[size(Table.value) - 2])));
				}
 				var sizeTable = size(Table.value);
 				S1.value = Table.value[sizeTable - 2] + ((E1.value - InputValues.value[sizeTable - 2]) * ((Table.value[sizeTable - 1] - Table.value[sizeTable - 2]) / (InputValues.value[sizeTable - 1] - InputValues.value[sizeTable - 2])));
 			}
 			compute compute_Lookup_InterpolationExtrapolation_above
 		}
 		mode Lookup_InterpolationExtrapolation_inside implements Lookup_InterpolationExtrapolation {
 			modeinvariant ocl {
				E1.value < InputValues.value->at(InputValues.value->size() - 1) and 
				E1.value > InputValues.value->at(0)
			}
			definition eml contract iter_final : TUInt8
			definition eml = compute_Lookup_InterpolationExtrapolation_inside {
				postcondition eml post_Lookup_InterpolationExtrapolation_inside_iter {
					InputValues.value[iter_final] <= E1.value && 
					E1.value <= InputValues.value[iter_final + 1];
				}
				postcondition eml post_Lookup_InterpolationExtrapolation_inside_final {
					S1.value == Table.value[iter_final] + ((E1.value - InputValues.value[iter_final]) * ((Table.value[iter_final + 1] - Table.value[iter_final]) / (InputValues.value[iter_final + 1] - InputValues.value[iter_final])));
				}
				var iter = 0;
				while (E1.value >= InputValues.value[iter + 1]){
					variant { size(InputValues.value) - iter }
					invariant { E1.value >= InputValues.value[iter] }
					invariant { 0 <= iter && iter < (size(InputValues.value)) }
					iter = iter + 1;
				}
				ghost iter_final = iter;
				assert { iter_final == iter}
				S1.value = Table.value[iter] + ((E1.value - InputValues.value[iter]) * ((Table.value[iter + 1] - Table.value[iter]) / (InputValues.value[iter + 1] - InputValues.value[iter])));
			}
			compute compute_Lookup_InterpolationExtrapolation_inside
 		}
 		
 		variant Lookup_InterpolationUseEndValues extends Lookup_Root {
			modeinvariant ocl {
				LookupMethod.value = !! LookupMethodEnum::InterpolationUseEndValues
			}
		}
 		mode Lookup_InterpolationUseEndValues_below implements Lookup_InterpolationUseEndValues {
 			modeinvariant ocl {
 				E1.value <= InputValues.value->at(0)
 			}
 			definition eml = compute_Lookup_InterpolationUseEndValues_below {
	 			postcondition eml post_Lookup_InterpolationUseEndValues_below_final {
	 				S1.value == Table.value[0];
	 			}
 				S1.value = Table.value[0];
 			}
 			compute compute_Lookup_InterpolationUseEndValues_below
 		}
 		mode Lookup_InterpolationUseEndValues_above implements Lookup_InterpolationUseEndValues {
 			modeinvariant ocl {
 				E1.value >= InputValues.value->at(InputValues.value->size() - 1)
 			}
 			definition eml = compute_Lookup_InterpolationUseEndValues_above {
	 			postcondition eml post_Lookup_InterpolationUseEndValues_above_final {
	 				S1.value == Table.value[size(InputValues.value) - 1];
	 			}
 				S1.value = Table.value[size(InputValues.value) - 1];
 			}
 			compute compute_Lookup_InterpolationUseEndValues_above
 		}
 		mode Lookup_InterpolationUseEndValues_inside implements Lookup_InterpolationUseEndValues {
 			modeinvariant ocl {
				E1.value < InputValues.value->at(InputValues.value->size() - 1) and 
				E1.value > InputValues.value->at(0)
			}
			definition eml contract iter_final : TUInt8
			definition eml = compute_Lookup_InterpolationUseEndValues_inside {
				postcondition eml post_Lookup_InterpolationUseEndValues_inside_iter {
					InputValues.value[iter_final] <= E1.value && 
					E1.value <= InputValues.value[iter_final + 1];
				}
				postcondition eml post_Lookup_InterpolationUseEndValues_inside_final {
					S1.value == Table.value[iter_final] + ((E1.value - InputValues.value[iter_final]) * ((Table.value[iter_final + 1] - Table.value[iter_final]) / (InputValues.value[iter_final + 1] - InputValues.value[iter_final])));
				}
				var iter = 0;
				while (E1.value >= InputValues.value[iter + 1]){
					variant { size(InputValues.value) - iter }
					invariant { E1.value >= InputValues.value[iter] }
					invariant { 0 <= iter && iter < (size(InputValues.value)) }
					iter = iter + 1;
				}
				ghost iter_final = iter;
				assert { iter_final == iter}
				S1.value = Table.value[iter] + ((E1.value - InputValues.value[iter]) * ((Table.value[iter + 1] - Table.value[iter]) / (InputValues.value[iter + 1] - InputValues.value[iter])));
			}
			compute compute_Lookup_InterpolationUseEndValues_inside
 		}
	}	
}
Auxiliary files: BlockLibrary Why3 theories

BlockLibrary specification uses embedded languages (OCL and an imperative action language) for constraints specification. Translation from BlockLibrary to the verification language (Why3) is done by relying on a set of custom theories developped in order to simplify the translation. These theories documentation is accessible at Why theories.

Output: Why3 theories

We are able to generate Why3 theories for each BlockType specification. For each BlockType, we also generate goals that express the completeness and the disjointness proof objectives. These objectives needs to be discharged in order to assess the consistency of the Block specification.

The current implementation uses a two-step process :

  1. Generation of the model of the properties, conforming to the Why3 meta-model, using a model-to-model transformation, written in Java using the EMF API.

    Transformation implementation in org.geneauto.blocklibrary.verificationGeneration.toWhy:

    Transformation run configuration:

    1. In an eclipse environment where the blockLibrary is installed, select one or multiple .bls specification files.

    #. In the BlockLibrary toolkit sub-menu, select Convert as Why3 theories and modules

    1. THe output why3 files are then generated in the why-gen sub-folder.

Serialisation of the Why3 model as text representation relies on the LogicalExpression grammar. tHis grammar is know to have some issues:

  • a < b < c is parsed as (a < b) < c instead of b in [a,c].

Previous implementation using an ATL transformation is located in org.geneauto.blocklibrary.alt.verificationGeneration.toWhy3

An even older implementation with Acceleo templates is located in org.geneauto.blocklibrary.verificationGeneration.toWhy.

Here is the generated code for the Lookup block specification generation:

theory Lookup_FeaturesDT "Generated from file:/home/arnaud/work/repositories/git_krates/blocklibrary/examples/BlockSpecs/SimpleBlocks.bls"

	use export SimpleBlocks_DataTypes . SimpleBlocks_DataTypes

	type tE1_Lookup_Root_TDouble = tInPortGroup (tRealDouble)
	type tS1_Lookup_Root_TDouble = tOutPortGroup (tRealDouble)
	type tInputValues_Lookup_Root_InputValuesType = tParameterType (list tRealDouble)
	type tTable_Lookup_Root_TableType = tParameterType (list tRealDouble)
	type tLookupMethod_Lookup_Root_LookupMethodEnum = tParameterType (lookupMethodEnum)
end
theory Lookup_InterpolationExtrapolation_below_sig0 "Generated from file:/home/arnaud/work/repositories/git_krates/blocklibrary/examples/BlockSpecs/SimpleBlocks.bls for BlockMode: Lookup_InterpolationExtrapolation_below"

	use export Lookup_FeaturesDT

	axiom Lookup_Lookup_Root_inputValuesOrdered :
	forall inputValues : tInputValues_Lookup_Root_InputValuesType . 
	let inputvalues_0 = inputValues . value_pt in 
	forall i1 : int . 
	let inputvalues_2 = inputValues . value_pt in 
	let inputvalues_3 = inputValues . value_pt in 
		0 <= i1 < length inputvalues_0 -> 
		inputvalues_0[i1] <> inputvalues_2[length inputvalues_2 - 1] -> 
		inputvalues_0[i1] <=. inputvalues_3[(
			let inputvalues_4 = inputValues . value_pt in 
				indexOf inputvalues_4 (inputvalues_0[i1]) + 1
		)]

	axiom Lookup_Lookup_Root_inv1 :
	forall inputValues : tInputValues_Lookup_Root_InputValuesType , table : tTable_Lookup_Root_TableType . 
	let inputvalues_0 = inputValues . value_pt in 
	let table_1 = table . value_pt in 
		length inputvalues_0 = length table_1

	axiom Lookup_Lookup_Root_inv2 :
	forall inputValues : tInputValues_Lookup_Root_InputValuesType . 
	let inputvalues_0 = inputValues . value_pt in 
	let inputvalues_1 = inputValues . value_pt in 
		inputvalues_0[0] <. inputvalues_1[(
			let inputvalues_2 = inputValues . value_pt in 
				length inputvalues_2 - 1
		)]

	axiom Lookup_Lookup_Root_inv3 :
	forall inputValues : tInputValues_Lookup_Root_InputValuesType . 
	let inputvalues_0 = inputValues . value_pt in 
	length inputvalues_0 > 0

	predicate lookup_interpolationextrapolation_modeInv_0 (table : tTable_Lookup_Root_TableType) (inputValues : tInputValues_Lookup_Root_InputValuesType) (s1 : tS1_Lookup_Root_TDouble) (e1 : tE1_Lookup_Root_TDouble) (lookupMethod : tLookupMethod_Lookup_Root_LookupMethodEnum) =
	lookupMethod . value_pt = InterpolationExtrapolation

	predicate lookup_interpolationextrapolation_below_modeInv_1 (table : tTable_Lookup_Root_TableType) (inputValues : tInputValues_Lookup_Root_InputValuesType) (s1 : tS1_Lookup_Root_TDouble) (e1 : tE1_Lookup_Root_TDouble) (lookupMethod : tLookupMethod_Lookup_Root_LookupMethodEnum) =
	let inputvalues_0 = inputValues . value_pt in 
		e1 . value_inpg <=. inputvalues_0[0]

	predicate lookup_InterpolationExtrapolation_below_sig0 (table : tTable_Lookup_Root_TableType) (inputValues : tInputValues_Lookup_Root_InputValuesType) (s1 : tS1_Lookup_Root_TDouble) (e1 : tE1_Lookup_Root_TDouble) (lookupMethod : tLookupMethod_Lookup_Root_LookupMethodEnum) =
	lookup_interpolationextrapolation_modeInv_0 table inputValues s1 e1 lookupMethod /\ lookup_interpolationextrapolation_below_modeInv_1 table inputValues s1 e1 lookupMethod
end
theory Lookup_InterpolationExtrapolation_above_sig0 "Generated from file:/home/arnaud/work/repositories/git_krates/blocklibrary/examples/BlockSpecs/SimpleBlocks.bls for BlockMode: Lookup_InterpolationExtrapolation_above"

	use export Lookup_FeaturesDT

	axiom Lookup_Lookup_Root_inputValuesOrdered :
	forall inputValues : tInputValues_Lookup_Root_InputValuesType . 
	let inputvalues_0 = inputValues . value_pt in 
	forall i1 : int . 
	let inputvalues_2 = inputValues . value_pt in 
	let inputvalues_3 = inputValues . value_pt in 
		0 <= i1 < length inputvalues_0 -> 
		inputvalues_0[i1] <> inputvalues_2[length inputvalues_2 - 1] -> 
		inputvalues_0[i1] <=. inputvalues_3[(
			let inputvalues_4 = inputValues . value_pt in 
				indexOf inputvalues_4 (inputvalues_0[i1]) + 1
		)]

	axiom Lookup_Lookup_Root_inv1 :
	forall inputValues : tInputValues_Lookup_Root_InputValuesType , table : tTable_Lookup_Root_TableType . 
	let inputvalues_0 = inputValues . value_pt in 
	let table_1 = table . value_pt in 
		length inputvalues_0 = length table_1

	axiom Lookup_Lookup_Root_inv2 :
	forall inputValues : tInputValues_Lookup_Root_InputValuesType . 
	let inputvalues_0 = inputValues . value_pt in 
	let inputvalues_1 = inputValues . value_pt in 
		inputvalues_0[0] <. inputvalues_1[(
			let inputvalues_2 = inputValues . value_pt in 
				length inputvalues_2 - 1
		)]

	axiom Lookup_Lookup_Root_inv3 :
	forall inputValues : tInputValues_Lookup_Root_InputValuesType . 
	let inputvalues_0 = inputValues . value_pt in 
		length inputvalues_0 > 0

	predicate lookup_interpolationextrapolation_modeInv_0 (table : tTable_Lookup_Root_TableType) (inputValues : tInputValues_Lookup_Root_InputValuesType) (s1 : tS1_Lookup_Root_TDouble) (e1 : tE1_Lookup_Root_TDouble) (lookupMethod : tLookupMethod_Lookup_Root_LookupMethodEnum) =
	lookupMethod . value_pt = InterpolationExtrapolation

	predicate lookup_interpolationextrapolation_above_modeInv_1 (table : tTable_Lookup_Root_TableType) (inputValues : tInputValues_Lookup_Root_InputValuesType) (s1 : tS1_Lookup_Root_TDouble) (e1 : tE1_Lookup_Root_TDouble) (lookupMethod : tLookupMethod_Lookup_Root_LookupMethodEnum) =
	let inputvalues_0 = inputValues . value_pt in 
		e1 . value_inpg >=. inputvalues_0[(
			let inputvalues_1 = inputValues . value_pt in 
				length inputvalues_1 - 1
		)]

	predicate lookup_InterpolationExtrapolation_above_sig0 (table : tTable_Lookup_Root_TableType) (inputValues : tInputValues_Lookup_Root_InputValuesType) (s1 : tS1_Lookup_Root_TDouble) (e1 : tE1_Lookup_Root_TDouble) (lookupMethod : tLookupMethod_Lookup_Root_LookupMethodEnum) =
	lookup_interpolationextrapolation_modeInv_0 table inputValues s1 e1 lookupMethod /\ lookup_interpolationextrapolation_above_modeInv_1 table inputValues s1 e1 lookupMethod
end
theory Lookup_InterpolationExtrapolation_inside_sig0 "Generated from file:/home/arnaud/work/repositories/git_krates/blocklibrary/examples/BlockSpecs/SimpleBlocks.bls for BlockMode: Lookup_InterpolationExtrapolation_inside"

	use export Lookup_FeaturesDT

	axiom Lookup_Lookup_Root_inputValuesOrdered :
	forall inputValues : tInputValues_Lookup_Root_InputValuesType . 
	let inputvalues_0 = inputValues . value_pt in 
	forall i1 : int . 
	let inputvalues_2 = inputValues . value_pt in 
	let inputvalues_3 = inputValues . value_pt in 
		0 <= i1 < length inputvalues_0 -> 
		inputvalues_0[i1] <> inputvalues_2[length inputvalues_2 - 1] -> 
		inputvalues_0[i1] <=. inputvalues_3[(
			let inputvalues_4 = inputValues . value_pt in 
				indexOf inputvalues_4 (inputvalues_0[i1]) + 1
		)]

	axiom Lookup_Lookup_Root_inv1 :
	forall inputValues : tInputValues_Lookup_Root_InputValuesType , table : tTable_Lookup_Root_TableType . 
	let inputvalues_0 = inputValues . value_pt in 
	let table_1 = table . value_pt in 
		length inputvalues_0 = length table_1

	axiom Lookup_Lookup_Root_inv2 :
	forall inputValues : tInputValues_Lookup_Root_InputValuesType . 
	let inputvalues_0 = inputValues . value_pt in 
	let inputvalues_1 = inputValues . value_pt in 
		inputvalues_0[0] <. inputvalues_1[(
			let inputvalues_2 = inputValues . value_pt in 
				length inputvalues_2 - 1
		)]

	axiom Lookup_Lookup_Root_inv3 :
	forall inputValues : tInputValues_Lookup_Root_InputValuesType . 
	let inputvalues_0 = inputValues . value_pt in 
		length inputvalues_0 > 0

	predicate lookup_interpolationextrapolation_modeInv_0 (table : tTable_Lookup_Root_TableType) (inputValues : tInputValues_Lookup_Root_InputValuesType) (s1 : tS1_Lookup_Root_TDouble) (e1 : tE1_Lookup_Root_TDouble) (lookupMethod : tLookupMethod_Lookup_Root_LookupMethodEnum) =
	lookupMethod . value_pt = InterpolationExtrapolation

	predicate lookup_interpolationextrapolation_inside_modeInv_1 (table : tTable_Lookup_Root_TableType) (inputValues : tInputValues_Lookup_Root_InputValuesType) (s1 : tS1_Lookup_Root_TDouble) (e1 : tE1_Lookup_Root_TDouble) (lookupMethod : tLookupMethod_Lookup_Root_LookupMethodEnum) =
	let inputvalues_0 = inputValues . value_pt in 
	let inputvalues_2 = inputValues . value_pt in 
		e1 . value_inpg <. inputvalues_0[(
			let inputvalues_1 = inputValues . value_pt in 
				length inputvalues_1 - 1
		)] /\ 
		e1 . value_inpg >. inputvalues_2[0]

	predicate lookup_InterpolationExtrapolation_inside_sig0 (table : tTable_Lookup_Root_TableType) (inputValues : tInputValues_Lookup_Root_InputValuesType) (s1 : tS1_Lookup_Root_TDouble) (e1 : tE1_Lookup_Root_TDouble) (lookupMethod : tLookupMethod_Lookup_Root_LookupMethodEnum) =
	lookup_interpolationextrapolation_modeInv_0 table inputValues s1 e1 lookupMethod /\ lookup_interpolationextrapolation_inside_modeInv_1 table inputValues s1 e1 lookupMethod
end
theory Lookup_InterpolationUseEndValues_below_sig0 "Generated from file:/home/arnaud/work/repositories/git_krates/blocklibrary/examples/BlockSpecs/SimpleBlocks.bls for BlockMode: Lookup_InterpolationUseEndValues_below"

	use export Lookup_FeaturesDT

	axiom Lookup_Lookup_Root_inputValuesOrdered :
	forall inputValues : tInputValues_Lookup_Root_InputValuesType . 
	let inputvalues_0 = inputValues . value_pt in 
	forall i1 : int . 
	let inputvalues_2 = inputValues . value_pt in 
	let inputvalues_3 = inputValues . value_pt in 
		0 <= i1 < length inputvalues_0 -> 
		inputvalues_0[i1] <> inputvalues_2[length inputvalues_2 - 1] -> 
		inputvalues_0[i1] <=. inputvalues_3[(
			let inputvalues_4 = inputValues . value_pt in 
				indexOf inputvalues_4 (inputvalues_0[i1]) + 1
		)]

	axiom Lookup_Lookup_Root_inv1 :
	forall inputValues : tInputValues_Lookup_Root_InputValuesType , table : tTable_Lookup_Root_TableType . 
	let inputvalues_0 = inputValues . value_pt in 
	let table_1 = table . value_pt in 
		length inputvalues_0 = length table_1

	axiom Lookup_Lookup_Root_inv2 :
	forall inputValues : tInputValues_Lookup_Root_InputValuesType . 
	let inputvalues_0 = inputValues . value_pt in 
	let inputvalues_1 = inputValues . value_pt in 
		inputvalues_0[0] <. inputvalues_1[(
			let inputvalues_2 = inputValues . value_pt in 
				length inputvalues_2 - 1
		)]

	axiom Lookup_Lookup_Root_inv3 :
	forall inputValues : tInputValues_Lookup_Root_InputValuesType . 
	let inputvalues_0 = inputValues . value_pt in 
		length inputvalues_0 > 0

	predicate lookup_interpolationuseendvalues_modeInv_0 (table : tTable_Lookup_Root_TableType) (inputValues : tInputValues_Lookup_Root_InputValuesType) (s1 : tS1_Lookup_Root_TDouble) (e1 : tE1_Lookup_Root_TDouble) (lookupMethod : tLookupMethod_Lookup_Root_LookupMethodEnum) =
	lookupMethod . value_pt = InterpolationUseEndValues

	predicate lookup_interpolationuseendvalues_below_modeInv_1 (table : tTable_Lookup_Root_TableType) (inputValues : tInputValues_Lookup_Root_InputValuesType) (s1 : tS1_Lookup_Root_TDouble) (e1 : tE1_Lookup_Root_TDouble) (lookupMethod : tLookupMethod_Lookup_Root_LookupMethodEnum) =
	let inputvalues_0 = inputValues . value_pt in 
		e1 . value_inpg <=. inputvalues_0[0]

	predicate lookup_InterpolationUseEndValues_below_sig0 (table : tTable_Lookup_Root_TableType) (inputValues : tInputValues_Lookup_Root_InputValuesType) (s1 : tS1_Lookup_Root_TDouble) (e1 : tE1_Lookup_Root_TDouble) (lookupMethod : tLookupMethod_Lookup_Root_LookupMethodEnum) =
	lookup_interpolationuseendvalues_modeInv_0 table inputValues s1 e1 lookupMethod /\ lookup_interpolationuseendvalues_below_modeInv_1 table inputValues s1 e1 lookupMethod
end
theory Lookup_InterpolationUseEndValues_above_sig0 "Generated from file:/home/arnaud/work/repositories/git_krates/blocklibrary/examples/BlockSpecs/SimpleBlocks.bls for BlockMode: Lookup_InterpolationUseEndValues_above"

	use export Lookup_FeaturesDT

	axiom Lookup_Lookup_Root_inputValuesOrdered :
	forall inputValues : tInputValues_Lookup_Root_InputValuesType . 
	let inputvalues_0 = inputValues . value_pt in 
	forall i1 : int . 
	let inputvalues_2 = inputValues . value_pt in 
	let inputvalues_3 = inputValues . value_pt in 
		0 <= i1 < length inputvalues_0 -> 
		inputvalues_0[i1] <> inputvalues_2[length inputvalues_2 - 1] -> 
		inputvalues_0[i1] <=. inputvalues_3[(
			let inputvalues_4 = inputValues . value_pt in 
				indexOf inputvalues_4 (inputvalues_0[i1]) + 1
		)]

	axiom Lookup_Lookup_Root_inv1 :
	forall inputValues : tInputValues_Lookup_Root_InputValuesType , table : tTable_Lookup_Root_TableType . 
	let inputvalues_0 = inputValues . value_pt in 
	let table_1 = table . value_pt in 
		length inputvalues_0 = length table_1

	axiom Lookup_Lookup_Root_inv2 :
	forall inputValues : tInputValues_Lookup_Root_InputValuesType . 
	let inputvalues_0 = inputValues . value_pt in 
	let inputvalues_1 = inputValues . value_pt in 
		inputvalues_0[0] <. inputvalues_1[(
			let inputvalues_2 = inputValues . value_pt in 
				length inputvalues_2 - 1
		)]

	axiom Lookup_Lookup_Root_inv3 :
	forall inputValues : tInputValues_Lookup_Root_InputValuesType . 
	let inputvalues_0 = inputValues . value_pt in 
		length inputvalues_0 > 0

	predicate lookup_interpolationuseendvalues_modeInv_0 (table : tTable_Lookup_Root_TableType) (inputValues : tInputValues_Lookup_Root_InputValuesType) (s1 : tS1_Lookup_Root_TDouble) (e1 : tE1_Lookup_Root_TDouble) (lookupMethod : tLookupMethod_Lookup_Root_LookupMethodEnum) =
	lookupMethod . value_pt = InterpolationUseEndValues

	predicate lookup_interpolationuseendvalues_above_modeInv_1 (table : tTable_Lookup_Root_TableType) (inputValues : tInputValues_Lookup_Root_InputValuesType) (s1 : tS1_Lookup_Root_TDouble) (e1 : tE1_Lookup_Root_TDouble) (lookupMethod : tLookupMethod_Lookup_Root_LookupMethodEnum) =
	let inputvalues_0 = inputValues . value_pt in 
		e1 . value_inpg >=. inputvalues_0[(
			let inputvalues_1 = inputValues . value_pt in 
				length inputvalues_1 - 1
		)]

	predicate lookup_InterpolationUseEndValues_above_sig0 (table : tTable_Lookup_Root_TableType) (inputValues : tInputValues_Lookup_Root_InputValuesType) (s1 : tS1_Lookup_Root_TDouble) (e1 : tE1_Lookup_Root_TDouble) (lookupMethod : tLookupMethod_Lookup_Root_LookupMethodEnum) =
	lookup_interpolationuseendvalues_modeInv_0 table inputValues s1 e1 lookupMethod /\ lookup_interpolationuseendvalues_above_modeInv_1 table inputValues s1 e1 lookupMethod
end
theory Lookup_InterpolationUseEndValues_inside_sig0 "Generated from file:/home/arnaud/work/repositories/git_krates/blocklibrary/examples/BlockSpecs/SimpleBlocks.bls for BlockMode: Lookup_InterpolationUseEndValues_inside"

	use export Lookup_FeaturesDT

	axiom Lookup_Lookup_Root_inputValuesOrdered :
	forall inputValues : tInputValues_Lookup_Root_InputValuesType . 
	let inputvalues_0 = inputValues . value_pt in 
	forall i1 : int . 
	let inputvalues_2 = inputValues . value_pt in 
	let inputvalues_3 = inputValues . value_pt in 
		0 <= i1 < length inputvalues_0 -> 
		inputvalues_0[i1] <> inputvalues_2[length inputvalues_2 - 1] -> 
		inputvalues_0[i1] <=. inputvalues_3[(
			let inputvalues_4 = inputValues . value_pt in 
				indexOf inputvalues_4 (inputvalues_0[i1]) + 1
		)]

	axiom Lookup_Lookup_Root_inv1 :
	forall inputValues : tInputValues_Lookup_Root_InputValuesType , table : tTable_Lookup_Root_TableType . 
	let inputvalues_0 = inputValues . value_pt in 
	let table_1 = table . value_pt in 
		length inputvalues_0 = length table_1

	axiom Lookup_Lookup_Root_inv2 :
	forall inputValues : tInputValues_Lookup_Root_InputValuesType . 
	let inputvalues_0 = inputValues . value_pt in 
	let inputvalues_1 = inputValues . value_pt in 
		inputvalues_0[0] <. inputvalues_1[(
			let inputvalues_2 = inputValues . value_pt in 
				length inputvalues_2 - 1
		)]

	axiom Lookup_Lookup_Root_inv3 :
	forall inputValues : tInputValues_Lookup_Root_InputValuesType . 
	let inputvalues_0 = inputValues . value_pt in 
		length inputvalues_0 > 0

	predicate lookup_interpolationuseendvalues_modeInv_0 (table : tTable_Lookup_Root_TableType) (inputValues : tInputValues_Lookup_Root_InputValuesType) (s1 : tS1_Lookup_Root_TDouble) (e1 : tE1_Lookup_Root_TDouble) (lookupMethod : tLookupMethod_Lookup_Root_LookupMethodEnum) =
	lookupMethod . value_pt = InterpolationUseEndValues

	predicate lookup_interpolationuseendvalues_inside_modeInv_1 (table : tTable_Lookup_Root_TableType) (inputValues : tInputValues_Lookup_Root_InputValuesType) (s1 : tS1_Lookup_Root_TDouble) (e1 : tE1_Lookup_Root_TDouble) (lookupMethod : tLookupMethod_Lookup_Root_LookupMethodEnum) =
	let inputvalues_0 = inputValues . value_pt in 
	let inputvalues_2 = inputValues . value_pt in 
		e1 . value_inpg <. inputvalues_0[(
			let inputvalues_1 = inputValues . value_pt in 
				length inputvalues_1 - 1
		)] /\ 
		e1 . value_inpg >. inputvalues_2[0]

	predicate lookup_InterpolationUseEndValues_inside_sig0 (table : tTable_Lookup_Root_TableType) (inputValues : tInputValues_Lookup_Root_InputValuesType) (s1 : tS1_Lookup_Root_TDouble) (e1 : tE1_Lookup_Root_TDouble) (lookupMethod : tLookupMethod_Lookup_Root_LookupMethodEnum) =
	lookup_interpolationuseendvalues_modeInv_0 table inputValues s1 e1 lookupMethod /\ lookup_interpolationuseendvalues_inside_modeInv_1 table inputValues s1 e1 lookupMethod
end
theory Lookup_Verif "Generated from file:/home/arnaud/work/repositories/git_krates/blocklibrary/examples/BlockSpecs/SimpleBlocks.bls"

	use import Lookup_InterpolationExtrapolation_below_sig0

	use import Lookup_InterpolationExtrapolation_above_sig0

	use import Lookup_InterpolationExtrapolation_inside_sig0

	use import Lookup_InterpolationUseEndValues_below_sig0

	use import Lookup_InterpolationUseEndValues_above_sig0

	use import Lookup_InterpolationUseEndValues_inside_sig0

	goal Lookup_completeness :
	forall table : tTable_Lookup_Root_TableType , inputValues : tInputValues_Lookup_Root_InputValuesType , s1 : tS1_Lookup_Root_TDouble , e1 : tE1_Lookup_Root_TDouble , lookupMethod : tLookupMethod_Lookup_Root_LookupMethodEnum . 
	lookup_InterpolationExtrapolation_below_sig0 table inputValues s1 e1 lookupMethod \/ 
	lookup_InterpolationExtrapolation_above_sig0 table inputValues s1 e1 lookupMethod \/ 
	lookup_InterpolationExtrapolation_inside_sig0 table inputValues s1 e1 lookupMethod \/ 
	lookup_InterpolationUseEndValues_below_sig0 table inputValues s1 e1 lookupMethod \/ 
	lookup_InterpolationUseEndValues_above_sig0 table inputValues s1 e1 lookupMethod \/ 
	lookup_InterpolationUseEndValues_inside_sig0 table inputValues s1 e1 lookupMethod

	goal Lookup_disjointness :
	forall table : tTable_Lookup_Root_TableType , inputValues : tInputValues_Lookup_Root_InputValuesType , s1 : tS1_Lookup_Root_TDouble , e1 : tE1_Lookup_Root_TDouble , lookupMethod : tLookupMethod_Lookup_Root_LookupMethodEnum . 
	not (
		lookup_InterpolationExtrapolation_below_sig0 table inputValues s1 e1 lookupMethod /\ 
		lookup_InterpolationExtrapolation_above_sig0 table inputValues s1 e1 lookupMethod) /\ 
	not (
		lookup_InterpolationExtrapolation_below_sig0 table inputValues s1 e1 lookupMethod /\ 
		lookup_InterpolationExtrapolation_inside_sig0 table inputValues s1 e1 lookupMethod) /\ 
	not (
		lookup_InterpolationExtrapolation_below_sig0 table inputValues s1 e1 lookupMethod /\ 
		lookup_InterpolationUseEndValues_below_sig0 table inputValues s1 e1 lookupMethod) /\ 
	not (
		lookup_InterpolationExtrapolation_below_sig0 table inputValues s1 e1 lookupMethod /\ 
		lookup_InterpolationUseEndValues_above_sig0 table inputValues s1 e1 lookupMethod) /\ 
	not (
		lookup_InterpolationExtrapolation_below_sig0 table inputValues s1 e1 lookupMethod /\ 
		lookup_InterpolationUseEndValues_inside_sig0 table inputValues s1 e1 lookupMethod) /\ 
	not (
		lookup_InterpolationExtrapolation_above_sig0 table inputValues s1 e1 lookupMethod /\
		lookup_InterpolationExtrapolation_inside_sig0 table inputValues s1 e1 lookupMethod) /\ 
	not (
		lookup_InterpolationExtrapolation_above_sig0 table inputValues s1 e1 lookupMethod /\ 
		lookup_InterpolationUseEndValues_below_sig0 table inputValues s1 e1 lookupMethod) /\ 
	not (
		lookup_InterpolationExtrapolation_above_sig0 table inputValues s1 e1 lookupMethod /\ 
		lookup_InterpolationUseEndValues_above_sig0 table inputValues s1 e1 lookupMethod) /\ 
	not (
		lookup_InterpolationExtrapolation_above_sig0 table inputValues s1 e1 lookupMethod /\ 
		lookup_InterpolationUseEndValues_inside_sig0 table inputValues s1 e1 lookupMethod) /\ 
	not (
		lookup_InterpolationExtrapolation_inside_sig0 table inputValues s1 e1 lookupMethod /\ 
		lookup_InterpolationUseEndValues_below_sig0 table inputValues s1 e1 lookupMethod) /\ 
	not (
		lookup_InterpolationExtrapolation_inside_sig0 table inputValues s1 e1 lookupMethod /\ 
		lookup_InterpolationUseEndValues_above_sig0 table inputValues s1 e1 lookupMethod) /\ 
	not (
		lookup_InterpolationExtrapolation_inside_sig0 table inputValues s1 e1 lookupMethod /\ 
		lookup_InterpolationUseEndValues_inside_sig0 table inputValues s1 e1 lookupMethod) /\ 
	not (
		lookup_InterpolationUseEndValues_below_sig0 table inputValues s1 e1 lookupMethod /\ 
		lookup_InterpolationUseEndValues_above_sig0 table inputValues s1 e1 lookupMethod) /\ 
	not (
		lookup_InterpolationUseEndValues_below_sig0 table inputValues s1 e1 lookupMethod /\ 
		lookup_InterpolationUseEndValues_inside_sig0 table inputValues s1 e1 lookupMethod) /\ 
	not (
		lookup_InterpolationUseEndValues_above_sig0 table inputValues s1 e1 lookupMethod /\ 
		lookup_InterpolationUseEndValues_inside_sig0 table inputValues s1 e1 lookupMethod)
end
Formal verification

This last file is fed into why3 and proof is done using an SMT solver (Alt-Ergo, CVC3, CVC4 and Z3 have been tested successfully).

Along with the generated .why files, are some copies of the BlockLibrary theories. In order to do the verification with why3, it is mandatory to provide the link to these files using the “include libraries” switch of why3: -L

The verification launch command and output of the verification are provided here:

$> why3 -L ./ -P alt-ergo SimpleBlocks_Lookup.why

SimpleBlocks_Lookup.why Lookup_Verif Lookup_completeness : Valid (0.12s)
SimpleBlocks_Lookup.why Lookup_Verif Lookup_disjointness : Valid (0.46s)

Semantics verification of the specification

From a BlockType specification, we can extract the set of Signatures. Each signature is related to a Hoare triple structure with

  • Pre conditions: invariants annotations on StructuralFeatures, mode_invariants annotations on BlockVariants and BlockMode, precondition annotations on each BlockMode semantics specification
  • Computation specification: specified in a BlockMode semantics specification
  • Post conditions: postconditions annotations on each BlockMode semantics specification

A signature can then be related to a function contract. The aim of this verification is to translate each signature to the corresponding function specification (with both function contract - pre/post; and function body).

As was previously presented, we are able to transform the blocklibrary structure and annotations to Why3. We use the same techniques to extract function contracts from the specification. The targeted language is no more the logical specification language Why3 but its complementary language WhyML.

Example 1

We provide an example of verification using the Abs block. This block is calculating the absolute value of its input. This is a very simple block but it illustrates well our approach.

The specification of the block with our BlockLibrary specification language is given here:

library ConstTest {
	typeDef realDouble myDouble
	blockType Abs {
		variant Abs_Root isDynamic {
			out S1 : myDouble
			in E1 : myDouble
		}
		mode BM1 implements Abs_Root {
			struct inv in matlab : "E1 < 0";
			compute : post in matlab : "S1 = - E1";
			backTyping : inv in matlab : "" ;
			forwardTyping : inv in matlab : "" ;
		}
		mode BM2 implements Abs_Root {
			struct inv in matlab : "E1 >= 0";
			compute : post in matlab : "S1 = E1";
			backTyping : inv in matlab : "" ;
			forwardTyping : inv in matlab : "" ;
		}
	}
}

Its translation into a WhyML contract is given here:

module Abs_Neg_sig0_computation "Generated from file:/home/arnaud/work/repositories/git_krates/blocklibrary/examples/BlockSpecs/Abs.bls for BlockMode: Abs_Neg"

	use import ConstTest_Abs . Abs_Neg_sig0

	let compute_Abs_Neg 
	(s1 : tS1_Abs_Root_TDouble) 
	(e1 : tE1_Abs_Root_TDouble) 
	requires { e1.value_pg <. 0.0 } 
	ensures { result >=. 0.0 } =
	0.0 -. e1.value_pg
end

module Abs_PosOrNul_sig0_computation "Generated from file:/home/arnaud/work/repositories/git_krates/blocklibrary/examples/BlockSpecs/Abs.bls for BlockMode: Abs_PosOrNul"

	use import ConstTest_Abs.Abs_PosOrNul_sig0

	let compute_Abs_PosOrNul 
	(s1 : tS1_Abs_Root_TDouble) 
	(e1 : tE1_Abs_Root_TDouble) 
	requires { e1.value_pg >=. 0.0 }
	ensures { result >=. 0.0 } = 
	e1.value_pg
end

The verification is automatically done using the Why tool and the alt-ergo SMT solver:

ConstTest_Abs_compute.mlw Abs_Neg_sig0_computation WP_parameter compute_Abs_Neg : Valid (0.06s)
ConstTest_Abs_compute.mlw Abs_PosOrNul_sig0_computation WP_parameter compute_Abs_PosOrNul : Valid (0.05s)

Example 2

We previously presented the Lookup block. From the BlockLibrary model presented below, we are able to generate a set of Why3 modules containing the semantics specification for the block:

module Lookup_FeaturesDTModule "Generated from file:/home/arnaud/work/repositories/git_krates/blocklibrary/examples/BlockSpecs/SimpleBlocks.bls"

	use export SimpleBlocks_DataTypesModule . SimpleBlocks_DataTypesModule

	type tE1_Lookup_Root_TDouble = tInPortGroup (tRealDouble)
	type tS1_Lookup_Root_TDouble = tOutPortGroup (tRealDouble)
	type tInputValues_Lookup_Root_InputValuesType = tParameterType (list tRealDouble)
	type tTable_Lookup_Root_TableType = tParameterType (list tRealDouble)
	type tLookupMethod_Lookup_Root_LookupMethodEnum = tParameterType (lookupMethodEnum)
end
module Lookup_InterpolationExtrapolation_below_sig0_computation "Generated from file:/home/arnaud/work/repositories/git_krates/blocklibrary/examples/BlockSpecs/SimpleBlocks.bls for BlockMode: Lookup_InterpolationExtrapolation_below"

	use import Lookup_FeaturesDTModule

	use import ref . Ref

	let compute_Lookup_InterpolationExtrapolation_below 
	(table : tTable_Lookup_Root_TableType) 
	(inputValues : tInputValues_Lookup_Root_InputValuesType) 
	(s1 : tS1_Lookup_Root_TDouble) 
	(e1 : tE1_Lookup_Root_TDouble) 
	(lookupMethod : tLookupMethod_Lookup_Root_LookupMethodEnum) 
	requires { 
		let inputvalues_0 = inputValues . value_pt in 
		forall i1 : int . 
		let inputvalues_2 = inputValues . value_pt in 
		let inputvalues_3 = inputValues . value_pt in 
			0 <= i1 < length inputvalues_0 -> 
			inputvalues_0[i1] <> inputvalues_2[length inputvalues_2 - 1] -> 
			inputvalues_0[i1] <=. inputvalues_3[(
				let inputvalues_4 = inputValues . value_pt in 
					indexOf inputvalues_4 (inputvalues_0[i1]) + 1
			)] 
	}
	requires { 
		let inputvalues_0 = inputValues . value_pt in 
		let table_1 = table . value_pt in 
			length inputvalues_0 = length table_1 
	} 
	requires { 
		let inputvalues_0 = inputValues . value_pt in 
		let inputvalues_1 = inputValues . value_pt in 
			inputvalues_0[0] <. inputvalues_1[(
				let inputvalues_2 = inputValues . value_pt in 
					length inputvalues_2 - 1
			)] 
	} 
	requires { 
		let inputvalues_0 = inputValues . value_pt in 
			length inputvalues_0 > 0 
	} 
	requires { 
		lookupMethod . value_pt = InterpolationExtrapolation 
	} 
	requires { 
		let inputvalues_0 = inputValues . value_pt in 
			e1 . value_inpg <=. inputvalues_0[0] 
	} 
	ensures { 
		s1 . value_outpg = table . value_pt[0] +. (e1 . value_inpg -. inputValues . value_pt[0]) *. ((table . value_pt[1] -. table . value_pt[0]) /. (inputValues . value_pt[1] -. inputValues . value_pt[0])) 
	} 
	= 
	s1 . value_outpg <- table . value_pt[0] +. (e1 . value_inpg -. inputValues . value_pt[0]) *. ((table . value_pt[1] -. table . value_pt[0]) /. (inputValues . value_pt[1] -. inputValues . value_pt[0]))
end
module Lookup_InterpolationExtrapolation_above_sig0_computation "Generated from file:/home/arnaud/work/repositories/git_krates/blocklibrary/examples/BlockSpecs/SimpleBlocks.bls for BlockMode: Lookup_InterpolationExtrapolation_above"

	use import Lookup_FeaturesDTModule

	use import ref . Ref

	let compute_Lookup_InterpolationExtrapolation_above 
	(table : tTable_Lookup_Root_TableType) 
	(inputValues : tInputValues_Lookup_Root_InputValuesType) 
	(s1 : tS1_Lookup_Root_TDouble) 
	(e1 : tE1_Lookup_Root_TDouble) 
	(lookupMethod : tLookupMethod_Lookup_Root_LookupMethodEnum) 
	requires { 
		let inputvalues_0 = inputValues . value_pt in 
		forall i1 : int . 
		let inputvalues_2 = inputValues . value_pt in 
		let inputvalues_3 = inputValues . value_pt in 
			0 <= i1 < length inputvalues_0 -> 
			inputvalues_0[i1] <> inputvalues_2[length inputvalues_2 - 1] -> 
			inputvalues_0[i1] <=. inputvalues_3[(
				let inputvalues_4 = inputValues . value_pt in 
					indexOf inputvalues_4 (inputvalues_0[i1]) + 1
			)] 
	} 
	requires { 
		let inputvalues_0 = inputValues . value_pt in 
		let table_1 = table . value_pt in 
			length inputvalues_0 = length table_1 
	} 
	requires { 
		let inputvalues_0 = inputValues . value_pt in 
		let inputvalues_1 = inputValues . value_pt in 
			inputvalues_0[0] <. inputvalues_1[(
				let inputvalues_2 = inputValues . value_pt in 
					length inputvalues_2 - 1
		)] 
	} 
	requires { 
		let inputvalues_0 = inputValues . value_pt in 
			length inputvalues_0 > 0 
	} 
	requires { 
		lookupMethod . value_pt = InterpolationExtrapolation 
	} 
	requires { 
		let inputvalues_0 = inputValues . value_pt in 
			e1 . value_inpg >=. inputvalues_0[(
				let inputvalues_1 = inputValues . value_pt in 
					length inputvalues_1 - 1
			)] 
	} 
	ensures { 
		s1 . value_outpg = table . value_pt[length (table . value_pt) - 2] +. (e1 . value_inpg -. inputValues . value_pt[length (table . value_pt) - 2]) *. ((table . value_pt[length (table . value_pt) - 1] -. table . value_pt[length (table . value_pt) - 2]) /. (inputValues . value_pt[length (table . value_pt) - 1] -. inputValues . value_pt[length (table . value_pt) - 2])) 
	} 
	= 
	let sizeTable_outer = length (table . value_pt) in 
	let sizeTable = ref sizeTable_outer in 
	s1 . value_outpg <- table . value_pt[! sizeTable - 2] +. (e1 . value_inpg -. inputValues . value_pt[! sizeTable - 2]) *. ((table . value_pt[! sizeTable - 1] -. table . value_pt[! sizeTable - 2]) /. (inputValues . value_pt[! sizeTable - 1] -. inputValues . value_pt[! sizeTable - 2]))
end
module Lookup_InterpolationExtrapolation_inside_sig0_computation "Generated from file:/home/arnaud/work/repositories/git_krates/blocklibrary/examples/BlockSpecs/SimpleBlocks.bls for BlockMode: Lookup_InterpolationExtrapolation_inside"

	use import Lookup_FeaturesDTModule

	use import ref . Ref

	val ghost iter_final : ref tRealUnSignedInt8 

	let compute_Lookup_InterpolationExtrapolation_inside 
	(table : tTable_Lookup_Root_TableType) 
	(inputValues : tInputValues_Lookup_Root_InputValuesType) 
	(s1 : tS1_Lookup_Root_TDouble) 
	(e1 : tE1_Lookup_Root_TDouble) 
	(lookupMethod : tLookupMethod_Lookup_Root_LookupMethodEnum) 
	requires { 
		let inputvalues_0 = inputValues . value_pt in 
		forall i1 : int . 
		let inputvalues_2 = inputValues . value_pt in 
		let inputvalues_3 = inputValues . value_pt in 
			0 <= i1 < length inputvalues_0 -> 
			inputvalues_0[i1] <> inputvalues_2[length inputvalues_2 - 1] -> 
			inputvalues_0[i1] <=. inputvalues_3[(
				let inputvalues_4 = inputValues . value_pt in 
					indexOf inputvalues_4 (inputvalues_0[i1]) + 1
			)] 
	} 
	requires { 
		let inputvalues_0 = inputValues . value_pt in 
		let table_1 = table . value_pt in 
			length inputvalues_0 = length table_1 
	} 
	requires { 
		let inputvalues_0 = inputValues . value_pt in 
		let inputvalues_1 = inputValues . value_pt in 
			inputvalues_0[0] <. inputvalues_1[(
				let inputvalues_2 = inputValues . value_pt in 
					length inputvalues_2 - 1
			)] 
	} 
	requires { 
		let inputvalues_0 = inputValues . value_pt in 
			length inputvalues_0 > 0 
	} 
	requires { 
		lookupMethod . value_pt = InterpolationExtrapolation 
	} 
	requires { 
		let inputvalues_0 = inputValues . value_pt in 
		let inputvalues_2 = inputValues . value_pt in 
			e1 . value_inpg <. inputvalues_0[(
				let inputvalues_1 = inputValues . value_pt in 
					length inputvalues_1 - 1
			)] /\ 
			e1 . value_inpg >. inputvalues_2[0] 
	} 
	ensures { 
		inputValues . value_pt[! iter_final] <=. e1 . value_inpg && 
		e1 . value_inpg <=. inputValues . value_pt[! iter_final + 1] 
	} 
	ensures { 
		s1 . value_outpg = table . value_pt[! iter_final] +. (e1 . value_inpg -. inputValues . value_pt[! iter_final]) *. ((table . value_pt[! iter_final + 1] -. table . value_pt[! iter_final]) /. (inputValues . value_pt[! iter_final + 1] -. inputValues . value_pt[! iter_final])) 
	} 
	= 
	let iter = ref 0 in 
	while e1 . value_inpg >=. inputValues . value_pt[! iter + 1] do 
		variant { length (inputValues . value_pt) - ! iter } 
		invariant { e1 . value_inpg >=. inputValues . value_pt[! iter] } 
		invariant { 0 <= ! iter && ! iter < length (inputValues . value_pt) } 
		iter := ! iter + 1 
	done ; 
	ghost iter_final := ! iter ; 
	assert { ! iter_final = ! iter } ; 
	s1 . value_outpg <- table . value_pt[! iter] +. (e1 . value_inpg -. inputValues . value_pt[! iter]) *. ((table . value_pt[! iter + 1] -. table . value_pt[! iter]) /. (inputValues . value_pt[! iter + 1] -. inputValues . value_pt[! iter]))
end
module Lookup_InterpolationUseEndValues_below_sig0_computation "Generated from file:/home/arnaud/work/repositories/git_krates/blocklibrary/examples/BlockSpecs/SimpleBlocks.bls for BlockMode: Lookup_InterpolationUseEndValues_below"

	use import Lookup_FeaturesDTModule

	use import ref . Ref

	let compute_Lookup_InterpolationUseEndValues_below (table : tTable_Lookup_Root_TableType) (inputValues : tInputValues_Lookup_Root_InputValuesType) (s1 : tS1_Lookup_Root_TDouble) (e1 : tE1_Lookup_Root_TDouble) (lookupMethod : tLookupMethod_Lookup_Root_LookupMethodEnum) requires { let inputvalues_0 = inputValues . value_pt in forall i1 : int . let inputvalues_2 = inputValues . value_pt in let inputvalues_3 = inputValues . value_pt in 0 <= i1 < length inputvalues_0 -> inputvalues_0[i1] <> inputvalues_2[length inputvalues_2 - 1] -> inputvalues_0[i1] <=. inputvalues_3[(let inputvalues_4 = inputValues . value_pt in indexOf inputvalues_4 (inputvalues_0[i1]) + 1)] } requires { let inputvalues_0 = inputValues . value_pt in let table_1 = table . value_pt in length inputvalues_0 = length table_1 } requires { let inputvalues_0 = inputValues . value_pt in let inputvalues_1 = inputValues . value_pt in inputvalues_0[0] <. inputvalues_1[(let inputvalues_2 = inputValues . value_pt in length inputvalues_2 - 1)] } requires { let inputvalues_0 = inputValues . value_pt in length inputvalues_0 > 0 } requires { lookupMethod . value_pt = InterpolationUseEndValues } requires { let inputvalues_0 =
	inputValues . value_pt in e1 . value_inpg <=. inputvalues_0[0] } ensures { s1 . value_outpg = table . value_pt[0] } = s1 . value_outpg <- table . value_pt[0]
end
module Lookup_InterpolationUseEndValues_above_sig0_computation "Generated from file:/home/arnaud/work/repositories/git_krates/blocklibrary/examples/BlockSpecs/SimpleBlocks.bls for BlockMode: Lookup_InterpolationUseEndValues_above"

	use import Lookup_FeaturesDTModule

	use import ref . Ref

	let compute_Lookup_InterpolationUseEndValues_above (table : tTable_Lookup_Root_TableType) (inputValues : tInputValues_Lookup_Root_InputValuesType) (s1 : tS1_Lookup_Root_TDouble) (e1 : tE1_Lookup_Root_TDouble) (lookupMethod : tLookupMethod_Lookup_Root_LookupMethodEnum) requires { let inputvalues_0 = inputValues . value_pt in forall i1 : int . let inputvalues_2 = inputValues . value_pt in let inputvalues_3 = inputValues . value_pt in 0 <= i1 < length inputvalues_0 -> inputvalues_0[i1] <> inputvalues_2[length inputvalues_2 - 1] -> inputvalues_0[i1] <=. inputvalues_3[(let inputvalues_4 = inputValues . value_pt in indexOf inputvalues_4 (inputvalues_0[i1]) + 1)] } requires { let inputvalues_0 = inputValues . value_pt in let table_1 = table . value_pt in length inputvalues_0 = length table_1 } requires { let inputvalues_0 = inputValues . value_pt in let inputvalues_1 = inputValues . value_pt in inputvalues_0[0] <. inputvalues_1[(let inputvalues_2 = inputValues . value_pt in length inputvalues_2 - 1)] } requires { let inputvalues_0 = inputValues . value_pt in length inputvalues_0 > 0 } requires { lookupMethod . value_pt = InterpolationUseEndValues } requires { let inputvalues_0 =
	inputValues . value_pt in e1 . value_inpg >=. inputvalues_0[(let inputvalues_1 = inputValues . value_pt in length inputvalues_1 - 1)] } ensures { s1 . value_outpg = table . value_pt[length (inputValues . value_pt) - 1] } = s1 . value_outpg <- table . value_pt[length (inputValues . value_pt) - 1]
end
module Lookup_InterpolationUseEndValues_inside_sig0_computation "Generated from file:/home/arnaud/work/repositories/git_krates/blocklibrary/examples/BlockSpecs/SimpleBlocks.bls for BlockMode: Lookup_InterpolationUseEndValues_inside"

	use import Lookup_FeaturesDTModule

	use import ref . Ref

	val ghost iter_final : ref tRealUnSignedInt8 let compute_Lookup_InterpolationUseEndValues_inside (table : tTable_Lookup_Root_TableType) (inputValues : tInputValues_Lookup_Root_InputValuesType) (s1 : tS1_Lookup_Root_TDouble) (e1 : tE1_Lookup_Root_TDouble) (lookupMethod : tLookupMethod_Lookup_Root_LookupMethodEnum) requires { let inputvalues_0 = inputValues . value_pt in forall i1 : int . let inputvalues_2 = inputValues . value_pt in let inputvalues_3 = inputValues . value_pt in 0 <= i1 < length inputvalues_0 -> inputvalues_0[i1] <> inputvalues_2[length inputvalues_2 - 1] -> inputvalues_0[i1] <=. inputvalues_3[(let inputvalues_4 = inputValues . value_pt in indexOf inputvalues_4 (inputvalues_0[i1]) + 1)] } requires { let inputvalues_0 = inputValues . value_pt in let table_1 = table . value_pt in length inputvalues_0 = length table_1 } requires { let inputvalues_0 = inputValues . value_pt in let inputvalues_1 = inputValues . value_pt in inputvalues_0[0] <. inputvalues_1[(let inputvalues_2 = inputValues . value_pt in length inputvalues_2 - 1)] } requires { let inputvalues_0 = inputValues . value_pt in length inputvalues_0 > 0 } requires { lookupMethod . value_pt =
	InterpolationUseEndValues } requires { let inputvalues_0 = inputValues . value_pt in let inputvalues_2 = inputValues . value_pt in e1 . value_inpg <. inputvalues_0[(let inputvalues_1 = inputValues . value_pt in length inputvalues_1 - 1)] /\ e1 . value_inpg >. inputvalues_2[0] } ensures { inputValues . value_pt[! iter_final] <=. e1 . value_inpg && e1 . value_inpg <=. inputValues . value_pt[! iter_final + 1] } ensures { s1 . value_outpg = table . value_pt[! iter_final] +. (e1 . value_inpg -. inputValues . value_pt[! iter_final]) *. ((table . value_pt[! iter_final + 1] -. table . value_pt[! iter_final]) /. (inputValues . value_pt[! iter_final + 1] -. inputValues . value_pt[! iter_final])) } = let iter = ref 0 in while e1 . value_inpg >=. inputValues . value_pt[! iter + 1] do variant { length (inputValues . value_pt) - ! iter } invariant { e1 . value_inpg >=. inputValues . value_pt[! iter] } invariant { 0 <= ! iter && ! iter < length (inputValues . value_pt) } iter := ! iter + 1 done ; ghost iter_final := ! iter ; assert { ! iter_final = ! iter } ; s1 . value_outpg <- table . value_pt[! iter] +. (e1 . value_inpg -. inputValues . value_pt[! iter]) *. ((table . value_pt[! iter + 1] -.
	table . value_pt[! iter]) /. (inputValues . value_pt[! iter + 1] -. inputValues . value_pt[! iter]))
end

The verification is done using the Why3 tool:

$ why3 -L ./ -P alt-ergo SimpleBlocks_Lookup_compute.mlw

SimpleBlocks_Lookup_compute.mlw Lookup_InterpolationExtrapolation_below_sig0_computation WP_parameter compute_Lookup_InterpolationExtrapolation_below : Valid (0.07s)
SimpleBlocks_Lookup_compute.mlw Lookup_InterpolationExtrapolation_above_sig0_computation WP_parameter compute_Lookup_InterpolationExtrapolation_above : Valid (0.07s)
SimpleBlocks_Lookup_compute.mlw Lookup_InterpolationExtrapolation_inside_sig0_computation WP_parameter compute_Lookup_InterpolationExtrapolation_inside : Valid (0.10s)
SimpleBlocks_Lookup_compute.mlw Lookup_InterpolationUseEndValues_below_sig0_computation WP_parameter compute_Lookup_InterpolationUseEndValues_below : Valid (0.06s)
SimpleBlocks_Lookup_compute.mlw Lookup_InterpolationUseEndValues_above_sig0_computation WP_parameter compute_Lookup_InterpolationUseEndValues_above : Valid (0.07s)
SimpleBlocks_Lookup_compute.mlw Lookup_InterpolationUseEndValues_inside_sig0_computation WP_parameter compute_Lookup_InterpolationUseEndValues_inside : Valid (0.09s)

Limitations

It is possible to extract the contracts from the specification. for simple examples there is no problem on the automatic verification side but for more complex code structure like loops, it is necessary to specify additional informations as loop variants and loop invariants. Loop varaints are really easy to specify but loop invariants are more difficult. Automatic techniques for the synthesis of loop invariants exists. We plan to use these techniques in order to complement our approach and verify the specification for more complex blocks.

On the methodology point of view, it is not mandatory to automatize this approach. The semantics specification writing can be done by hand (especially the loop invariants writing) by experts. As soon as the specification is written, it is possible to verify it automatically and formally. Then the specification is complete and can be used for further purposes like:

  • Automatic code generation verification
  • Automatic generation of documentation
  • Specification and qualification data generation