GeneAuto metamodel with verification annotations documentation

Overall picture

../_images/geneautoAnnot.png

geneauto::emf::models::gavamodel package

This package contains the necessary elements for the declaration of verificaiton annotations elements.

VAElement

VAElement extends the Annotation generic element. Its purpose is to hold annotations. These annotations will be printed on each code element.

CompoundVAElement

An abstract VAElement for holding compound annotations. These annotations will be made up of a set of AnnotationStatement.

References

annotStmts is containment for AnnotationStatement [1..*]

The AnnotationStatements.

SimpleVAElement

An abstract VAElement for holding simple annotations. These annotations will be made up of only one AnnotationStatement.

References

annotStmt is containment for AnnotationStatement [1..1]

The AnnotationStatement element used in the SimpleVAElement.

Contract

A contract is a high level construct used to gather a set of annotations that will have a common purpose.

LogicSpecification

A logic specification annotation.

LoopContract

A Loop contract. Used to specify loop behavior. Will contain at least a loop variant and a loop invariant.

AssertClause

AssertClauses are used for assert-like annotations.

GhostCode

GhostCode elements are used for annotations that behave as regular C code but only visible from specification.

TypeInvariant

A type invariant is used to specify invariants on types.

LetExpression

A VAElement for the declaration of variables usables in annotations.

Attributes

nameSpace: NameSpace [1..1]

References

statements is containment for VAElement [0..*]

A set of statements for the declaration of elements in the let expression.

geneauto::emf::models::gavamodel::statement package

This package contains the low level elements for the definition of annotation statement.

AnnotationStatement

The abstract class for annotation statements.

References

quantifier is reference to VAQuantifier [0..1]

An optional quantifier.

Assigns

The assign statement. Elements described in an assign statement are the only one that are assigned during the computation of the annotated code.

References

vars is reference to CodeModelVariable [1..*]

LoopAssign

A special form of the assign statement used only in loops.

Assumes

The assumes statement. In a behavior description, assume statements provides pre conditions.

References

subStatement is containment for AnnotationStatement [1..1]

Contained annotation statement.

Behavior

A behavior annotation. In a function contract the specified behavior might be splitted in multiple parts if the semantics might be modified during the computation. Behavior are used only in function contracts.

References

lstAssumeStatements is containment for Assumes [1..*]

The list of assume statements.

lstEnsuresStatements is containment for Ensures [1..*]

The list of ensures statements.

Ensures

The ensures statement. An ensure statement is a post condition expressed for the annotated code.

References

subStatement is containment for AnnotationStatement [1..1]

Contained annotation statement.

Ghost

A ghost statement. Ghost code is a set of code visible by all annotations in its scope. This code is used in order to define variables that are modified during the computation.

References

expr is reference to Expression [1..1]

GlobalInvariant

The global invariant statement. A global invariant expresses a property that must hold true during the whole computation.

References

subStatement is containment for AnnotationStatement [1..1]

Contained annotation statement.

LoopInvariant

The loop invariant statement. A loop invariant is an annotation used in loop computation. The loop invariant must be true right before entering the loop, must hold true after each step of the loop and so right after the computation of the loop.

References

subStatement is containment for AnnotationStatement [1..1]

Contained annotation statement.

LoopVariant

The loop variant annotation. Used only in loop annotations, this variant must be of integer type, be strictly positive while entering the loop and must be trictly decreasing.

References

expr is reference to Expression [1..1]

Requires

The require statement. These annotations are pre conditions for the computation of the annotated code.

References

subStatement is containment for AnnotationStatement [1..1]

Contained annotation statement.

Exists

The existential quantifier. Used in order to specify that a set of elements must exist in the context of the annotation statement.

References

lstVars is reference to CodeModelVariable [1..*]

ForAll

The universal existency quatifier. Used in order to specify that for a set of elements the anntoation statement is always verified.

References

lstVars is reference to CodeModelVariable [1..*]

lstRanges is reference to RangeExpression [1..*]

Valid

The valid statement. Element used in the valid statement must be valid in the sense that they must be accessible in memory.

References

var is reference to CodeModelVariable [1..1]

ValidRange

A valid range statement. Specify a valid range for a variable in which a multi-dimensional variable (array) is valid (in the sense of the Valid statement) for each component of the variable.

References

var is reference to CodeModelVariable [1..1]

range is reference to RangeExpression [1..1]

VAQuantifier

Quantifiers are used for quantification of annotations.