Generation of VCs for state actions

[treiher]

The VCs for each action in a session state is generated. The VCs are used in the code generator to add checks to ensure that the needed properties are fulfilled.

Model

Action	VC
X := Func (Y)	preconditions of expression Y
X := P::M (Y.Data)	"P.Contains.M_In_Y_Type_Data (Y)"
X := Y'Head	"Has_Element (Y)"
X := [for E in Y if E.Z => E]	Y'Valid
X := [for E in M.Y if E.Z => E]	M.Y'Valid
X := P::M'(A => Y, B => 1, C => [42])	path condition of P::M with A = Y, B = 1 and C = [42], and A = Y and B = 1 -> C'Size = [42]'Size
X := X + Y	X + Y <= X'Type'Last
X := X - Y	X - Y >= X'Type'First
X := Y.Z	Y.Z'Valid
X'Append (Y)	available space in X >= Y'Size
X'Append (P::M'(A => Y, B => 1, C => [42]))	path condition of P::M with A = Y, B = 1 and C = [42], and A = Y and B = 1 -> C'Size = [42]'Size, and available space in >= size of message
X	``

SPARK

• If an action has VCs, the preconditions are checked before the actual code for the action is executed.
• If a precondition is not fulfilled, the execution is aborted and the state is changed according to the exception transition.
• Optimization: Filter out statically true checks.