Go home now Header Background Image
Submission Procedure
share: |
Follow us
Volume 12 / Issue 10

available in:   PDF (125 kB) PS (113 kB)
Similar Docs BibTeX   Write a comment
Links into Future
DOI:   10.3217/jucs-012-10-1413


Proving Properties for Behavioural Specifications with Term Observation

Narjes Berregeb (Institut National des Sciences Appliquées et de Technologie, Tunisia)

Abstract: 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.

Keywords: behavioural specifications, covering contexts, observable contexts, term observation

Categories: F.3.1, F.4.1