Observational implementation of algebraic specifications (Q911245): Difference between revisions
From MaRDI portal
Set profile property. |
Set OpenAlex properties. |
||
(One intermediate revision by one other user not shown) | |||
Property / cites work | |||
Property / cites work: A systematic study of models of abstract data types / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: On the algebraic definition of programming languages / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3906394 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3947104 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3221381 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Algebraic implementation of abstract data types / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Parameterized Specifications: Parameter Passing and Implementation with Respect to Observability / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3742703 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4105777 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3956373 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3962973 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3707384 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4729318 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3938468 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3677153 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4721633 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3954805 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Structured algebraic specifications: A kernel language / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: On hierarchies of abstract data types / rank | |||
Normal rank | |||
Property / full work available at URL | |||
Property / full work available at URL: https://doi.org/10.1007/bf01178505 / rank | |||
Normal rank | |||
Property / OpenAlex ID | |||
Property / OpenAlex ID: W2062384035 / rank | |||
Normal rank |
Latest revision as of 08:22, 30 July 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Observational implementation of algebraic specifications |
scientific article |
Statements
Observational implementation of algebraic specifications (English)
0 references
1991
0 references
An observational approach to the construction of implementations of algebraic specifications is presented. Based on the theory of observational specifications an implementation relation is defined which formalizes the intuitive idea that an implementation is correct if it produces correct observable output. To be useful in practice proof theoretic criteria for observational implementations are provided and a proof technique (called ``context induction'') for the verification of implementation relations is presented. As an example an abstract specification of (the algebraic semantics of) a small imperative programming language is implemented by a state oriented specification of the language. In order to support the modular construction of implementations the approach is extended to parameterized observational specifications. Based on the notion of observable parameter context a proof theoretic criterion for parameterized observational implementations is presented and it is shown that under appropriate conditions observational implementations compose horizontally. The given implementation criteria are applied to examples.
0 references
algebraic specifications
0 references
observational implementations
0 references
verification
0 references
0 references