[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   
-------------------------------------------------------------------