Download Spec2Box - Adelard

Error messages
6.9
Denition and declaration structure errors
Such errors concern the structure of declarations and
denitions and can arise when an inconsistency in this
structure has been detected.
An example of this is when an explicit function is said to have
two parameters in its type, but its denition then gives three
parameters instead.
C.1
Repeated global declaration of <kind> <name>
A redeclaration has been encountered for a globally
declared VDM object of type kind and called name.
C.2
Multiple local decl. of pattern identifier
<name>
The named item is declared more than once in the same
local declaring context. This error generally arises
within patterns in cases and formal parameter lists.
C.3
Local declaration(s) fail to bind any variables
A local declaration (i.e. binding or pattern match) failed
to dene any variables in a context in which it is required
to do so, such as formal parameter lists and quantiers.
C.4
"MatchValue" pattern occurs in an erroneous
context
The `MatchValue' pattern occurs inside a pattern
expression where the overall context forbids its use.
SpecBox User Manual, version: PC/2.21a