Re: Predicate subtypes

[Mark Lawford <lawford@mcmaster.ca>]

Hi Pertti.

I think that your problem is arising from the type of px.  It is only
defined for arguments of type (p) so you need to use dependent typing in
"f1" to restrict "now" to values for which px(cc,next) is defined. 

The following modification of your theory eliminates the unprovable tcc. 


pred_type[st: TYPE, c: TYPE, p: [c, st -> bool], px: [(p) -> int]]: THEORY
 BEGIN

  f1: bool = FORALL (next: st, cc: c, now:{x:st|p(cc,x)}): p(cc, next) AND
px(cc, now) = 0
 END pred_type

Hope this helps,
Mark

Dr. Mark Lawford
Assistant Professor                        Email: lawford@McMaster.ca
DEPARTMENT OF COMPUTING AND SOFTWARE       Tel: 905 525 9140 Ext. 24911
Faculty of Engineering                     Fax: 905 524 0340
McMaster University,                       Office: JHE 302/C
Hamilton, Ontario  Canada L8S 4K1          http://www.cas.mcmaster.ca/~lawford

On Wed, 18 Apr 2001, Kellom{ki Pertti wrote:

> I am using predicate subtypes to model hierarchical state machines
> with embedded variables. By accident, I stumbled on the following
> behavior of PVS. The following theory typechecks and gives the
> expected (unprovable) TCC:
> 
> pred_type[st: TYPE, c: TYPE, p: [c, st -> bool], px: [(p) -> int]]: THEORY
>  BEGIN
> 
>   f1: bool = FORALL (now, next: st, cc: c): p(cc, next) AND px(cc, now) = 0
>  END pred_type
> 
> % Subtype TCC generated (at line 4, column 63) for  (cc, now)
>   % untried
> f1_TCC1: OBLIGATION
>   FORALL (cc: c, next: st, now): p(cc, next) IMPLIES p(cc, now);
> 
> It would seem reasonable to allow a (c,st) pair to be constrained with
> predicate p. What puzzles me is that also the following typechecks and
> gives the same TCC, even though the type of px is different.
> 
> pred_type2[st: TYPE, c: TYPE, p: [c, st -> bool], px: [(p) -> [st->int]]]: THEORY
>  BEGIN
> 
>   f1: bool = FORALL (now, next: st, cc: c): p(cc, next) AND px(cc, now) = 0
>  END pred_type2
> 
> % Subtype TCC generated (at line 4, column 63) for  (cc, now)
>   % untried
> f1_TCC1: OBLIGATION
>   FORALL (cc: c, next: st, now): p(cc, next) IMPLIES p(cc, now);
> 
> Can one use predicate subtypes in this way at all? If so, is there
> some implicit type conversion going on that I am not aware of?
> 
> Thanks,
> 	Pertti
>