Context induction: A proof principle for behavioural abstractions and algebraic implementations (Q1179807): Difference between revisions
From MaRDI portal
Changed an Item |
Set profile property. |
||
| Property / MaRDI profile type | |||
| Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank | |||
Revision as of 23:34, 4 March 2024
scientific article
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | Context induction: A proof principle for behavioural abstractions and algebraic implementations |
scientific article |
Statements
Context induction: A proof principle for behavioural abstractions and algebraic implementations (English)
0 references
27 June 1992
0 references
A context induction method is proposed and discussed. The method is appropriate for proving behavioural properties of data types. The motivation is supported by the fact that from a program user's point of view, internal data representations are not relevant if they induce the same observable effects. The applications for the proof technique using context induction principle are discussed as well. It is proposed to use context induction as a uniform proof principle in the process of formal program development.
0 references
behavioural specification
0 references
behavioural theorem
0 references
behavioural implementation
0 references
FRI implementation
0 references
