Typecheck question

[Tamarah Arons <tamarah@wisdom.weizmann.ac.il>]

Hello,

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?

I am using PVS2-3, no patches, on Rehat Linux 5.1

Thanks,
Tamarah
_____________________________________________________________________

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

---

• Prev by Date: two problems running PVS
• Next by Date: Re: Typecheck question
• Prev by thread: Re: How to prove this
• Next by thread: Re: Typecheck question
• Index(es):
  • Date
  • Thread