[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] Relation operations

Hi, I'm looking for domain/range operations on binary relations.  In
particular the operation "domain subtraction", where, for some
binary relation R on type (T1, T2), and some element x of type T1,
"dom_sub(R, x)" is a subset of R containing all all elements of R whose
first field is not x.

Domain subtraction is part of the Z specification language.  I can
see how to define it myself, but thought someone else might have
already formalised some part of Z in PVS (or perhaps I just missed
them in the prelude/mailing lists).