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

[PVS-Help] Fwd: type judgements

Just wanted to ping the list to see if there any suggestions w.r.t.
the original query...

---------- Forwarded message ----------
From: Stan Rosenberg <stan.rosenberg@xxxxxxxxx>
Date: Sat, Jun 23, 2012 at 4:30 PM
Subject: type judgements
To: pvs-help@xxxxxxxxxxx


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]?