Proving Properties for Behavioural Specifications with Term Observation
Дата
Авторы
Berregeb,Narjes
Journal Title
Journal ISSN
Volume Title
Издатель
Journal of Universal Computer Science
Аннотация
Описание
Behavioural specifications allow to focus only on the"observable" behaviour of objects. These observations are made through "observable contexts" which are particular terms with a hole to be filled in with an object. We consider behavioural specifications based on the observation of a specified set of linear terms. The set of observable contexts is often infinite; therefore, we give an algorithm for computing some special contexts that we call "covering contexts", and show that they are sufficient for proving that two terms are behaviourally equal.
Ключевые слова
behavioural specifications , term observation , observable contexts , covering contexts