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

*To*: pvs-help@csl.sri.com*Subject*: subtyping problem*From*: Jean-Paul BODEVEIX <bodeveix@irit.fr>*Date*: Fri, 31 Oct 1997 16:43:32 +0100*Sender*: bodeveix@irit.fr

I am surprised by the proof obligations generated by the following example where I define two predicates p and q with (q) <: (p) ie. (q) is a subtype of (p) Then I define the function f with an argument of type (q) which is initialised by a lambda expression with an argument of type (p). The initialization should be correct if the type of the rhs value is a subtype of the type of the lhs value. However, PVS requires the types to be identical (f_TCC3). Why ? Furthermore the TCC (1) seems inverted : it requires (p) :< (q). Thanks for any help JP Bodeveix University Paul Sabatier 118 route de Narbonne 31062 Toulouse - FRANCE ------------------------------------------------------------------------ subtype: THEORY BEGIN p: pred[nat] = (LAMBDA (x: nat): x > 0) q: pred[nat] = (LAMBDA (x: nat): x > 1) % Subtype TCC generated (line 8) for x: (p) f_TCC1: OBLIGATION (FORALL (x: (p)): q(x)); % Subtype TCC generated (line 8) for x - 1 f_TCC2: OBLIGATION (FORALL (x: (p)): x - 1 >= 0); % Domain mismatch subtype TCC generated (line 8) for (LAMBDA (x: (p)): x - 1) f_TCC3: OBLIGATION (FORALL (x1: (p), y1: (q)): p(y1) AND q(x1)); f: [(q) -> nat] = (LAMBDA (x: (p)): x - 1) END subtype

- Prev by Date:
**TCCs** - Next by Date:
**Re: subtyping problem** - Prev by thread:
**equality on characters** - Next by thread:
**Re: subtyping problem** - Index(es):