Responsible: Thomas Richter, Karsten Stahl,
Martin Steffen, all others
too
Only syntactically correct systems can be meaningfully processed, in our
case simulated. The task of this package is to check syntactical
consistency. The task comprises the definition of what syntactical
correctness means, i.e., what is guaranteed/checked by this group upon
which the others can rely on.
Interface
With the gui. The gui has to take care that the packages for
graph-placement, simulation, model-checking, code-generation ...are
handed over only checked syntax. What needs not to be checked are
``graphical lapses'', e.g., whether the nodes are placed one over the other
or similar things.
Contract
The checker assures well-typedness of expressions. The languages is rather
simple and the abstract syntax of Section A only
features integers and booleans and no scopes. We assume that the language
is well-typed. The types of the operators is shown in
Table 1.
operator/constant
type(s)
true,false
Bool
0,1,...
Int
+,*,/
Int × Int ® Int
-
Int × Int ® Int, Int®Int
<,>,£,³
Int ×Int ® Bool
=, ¹
Int×Int ® Bool, Bool×Bool®Bool
¬
Bool® Bool
Table 1: Types
Besides (and prior to) type-checking, the checker detects also various
situations, when the programs is considered to be ill-formed. The checker
guarantees, that
the sfc is non-null,
the (unique) initial step is contained in the set of steps,
all steps and transitions are non-null,
no step occurs twice (by name), and
no transition has a non-existing step as source or target (by name)
Note that test of non-nullness is not done for parts other than mentioned
(for instance sap's etc.)
