In this paper formal combined denotational-axiomatic semantics of the
canonical information model (SYNTHESIS labguage) is presented.
Canonical model abstract syntax, semantic domains and semantic functions
producing state space of a system specified by canonical specification are considered.
Semantic functions producing state space restrictions as well as
semantic functions producing predicates which correspond to methods
of Abstract Data Types (ADT) are defined.
Formal semantics developed allow to carry out provable reasoning
on information source model properties, such as consistency, refinement or correctness of
mapping of information models.
|
