Context induction: A proof principle for behavioural abstractions and algebraic implementations (Q1179807)

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.