[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Typecheck question
Tamarah,
> In the following file I *DO NOT* get a typecheck on the assignment
> of "R" to "count" in predicate a.
> Since R may be greater than C why isn't a typecheck generated?
>
> question[R, U, Z, B, P, C: posnat]: THEORY
> BEGIN
> VALUE: TYPE = real
>
> upto(m:posnat) : TYPE = {i:nat | i >= 0 and i <= m} CONTAINING m
> count_TYPE : TYPE = upto[C]
>
> PH_REG_ID: TYPE = upto[P]
> RF_ENTRY_TYPE: TYPE = [# v: VALUE, count: count_TYPE #]
> RF_TYPE: TYPE = [PH_REG_ID -> RF_ENTRY_TYPE]
>
> a(RF : RF_TYPE) : boolean =
> (FORALL (pr: PH_REG_ID): RF(pr) = (# v := 0, count := R #) )
> END question
The answer to your question is the semantics of equality expressions.
See the "PVS Language Reference" on p.40:
"[Equality and disequality] are both polymorphic, the type depending
on the types of the left- and right-hand sides. If the types are
compatible, meaning that there is a common supertype, then the
(dis)equality is of the greatest common supertype."
In your case, RF(pr) is of type [# v: VALUE, count: count_TYPE #],
while (# v := 0, count := R #) is of type [# v:nat, count:posnat #]
which are perfectly compatible.
So PVS does not generate a type-correctness condition (TCC) for the
expression (# v := 0, count := R #) because you didn't state that you
want it to be of type RF_ENTRY_TYPE. You can do so by adding a type
coercion: if you use
(# v := 0, count := R #)::RF_ENTRY_TYPE
on the right-hand side of the equality, you'll get the TCC you wanted.
Regards,
- Holger
--
-------------------------------------------------------------------
Holger Pfeifer Tel.: +49 (0)731 / 50-24124
Universität Ulm Fax: +49 (0)731 / 50-24119
Abt. Künstliche Intelligenz pfeifer@ki.informatik.uni-ulm.de
D-89069 Ulm http://www.informatik.uni-ulm.de/ki/pfeifer.html
-------------------------------------------------------------------