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

Re: [PVS-Help] extend



Extend is used to make the types match.  In your original specification

f: FUNCTION[S, set[A] -> T]
unchanged?(pre, post: S, K: set[A]): bool =
   FORALL (k: (K)): f(pre, singleton(k)) = f(post, singleton(k))

PVS has to infer the type of "singleton."  PVS will take the type of
the parameter k and use it as the type of singleton, that is, (K).
However, this type does not agree with the type of the second
parameter of "f."  So PVS needs to "extend" the type of singleton to
match set[A].

In your second example, PVS once again has to infer the type of
singleton, and once again uses the type of k.  However, this time
since the type of k is set[A], and since this matches the second
parameter of f, no extend needs to be inserted.

In this example, PVS will insert the "extend" because it knows that
(K) is a subtype of set[A].  If it didn't know this, then it would
generate a TCC and force you to prove the subtype relationship.

Another way to get rid of the "extend" is to explicitly give the type
of singleton, something like:

unchanged?(pre, post: S, K: set[A]): bool =
   FORALL (k: (K)): f(pre, singleton[A](k)) = f(post, singleton[A](k))

I tend to use types of the greatest supertype available, instead of
capturing this information in subtypes like (K).  Therefore I would
use your specification from below, to avoid type incompatibilities
that cause "extend" and "restrict" to be inserted.

To answer your second question, these forms are essentially the same,
except different types are involved.

Jeff

On Tue, Sep 1, 2009 at 3:02 PM, Jerome White<jerome@cs.caltech.edu> wrote:
> I was able to get rid of 'extend' by altering the definittion
> unchanged?:
>
>   unchanged?(pre, post: S, K: set[A]): bool =
>     FORALL (k: A): member(k, K) IMPLIES
>       f(pre, singleton(k)) = f(post, singleton(k))
>
> so, aside from wondering what extend means, I don't think I have a
> real understanding of what '(K)' means either. I was under the
> impression that the following were equivalent:
>
>  FORALL (k: A): member(k, K) IMPLIES B
>  FORALL (k: A | member(k, K): B
>  FORALL (k: (K)): B
>
> where 'B' is some boolean.
>
> jerome
>
> On Thu, Aug 27, 2009 at 08:54:32PM -0700, Jerome White wrote:
>>I have the following definition:
>>
>>  S, A, T: TYPE
>>  f: FUNCTION[S, set[A] -> T]
>>  % ...
>>  unchanged?(pre, post: S, K: set[A]): bool =
>>    FORALL (k: (K)): f(pre, singleton(k)) = f(post, singleton(k))
>>
>>When 'unchanged?' is opened in a proof, I get the following:
>>
>>  [1]   unchanged?(pre!1, post!1, complement(add(t!1, B!1)))
>>  Rule? (rewrite "unchanged?")
>>  {1}   FORALL (j: (complement(add(t!1, B!1)))):
>>       f(pre!1,
>>           extend[A, (complement(add(t!1, B!1))), bool, FALSE]
>>               (singleton(j)))
>>          =
>>          f(post!1,
>>            extend[A, (complement(add(t!1, B!1))), bool, FALSE]
>>                      (singleton(j)))
>>
>>What exactly is 'extend'? I see it in the prelude, but am unsure of
>>what it means in this context and why it's popping up. Any insight
>>would be much appreciated. Thanks
>>
>>jerome
>>
>
>