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

[PVS-Help] type judgements


I have defined the following predicate:

index_of?(s: finseq[real])(I: set[nat]): bool = forall (i: nat): I(i)
implies 0 <= i and i < s`length

This facilitates declarations like the following: foo(s: finseq[real],
I: (index_of?(s)))...

However, in many contexts it is expected that I be finite_set, yet
type judgements like the following are not allowed in pvs:

index_is_finite: JUDGEMENT (index_of?(s)) HAS_TYPE finite_set[nat]

Is there an alternative which would help avoid the generation of many
TCCa all requiring that I: (index_of?(s)) is finite_set[nat]?