|
Abstract : |
Where a concurrent system Impl is parameterised by a data type X with respect to which it is data independent, it is often possible to prove that Impl has a property Spec for all X by verifying it for a nite number of instantiations of X (a threshold collection). In this paper we show how to extend the denition of data independence for CSP to allow concurrent systems to include symbols representing generalised predicates, i.e. mappings from the type X to xed nite types such as the two-element type of booleans. Some of the main theorems that provide threshold collections, which were originally proved for data independence without these symbols, are revised for this extension., |
