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

*To*: Jean-Paul BODEVEIX <bodeveix@irit.fr>*Subject*: Re: subtyping problem*From*: Darrell Kindred <dkindred@cmu.edu>*Date*: Fri, 31 Oct 1997 11:37:41 -0500*Cc*: pvs-help@csl.sri.com*In-Reply-To*: <3459FCA4.1792@irit.fr>*Organization*: Carnegie Mellon University School of Computer Science*References*: <3459FCA4.1792@irit.fr>

Jean-Paul BODEVEIX writes: > 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 In PVS, the domains of two functions must be exactly the same for the functions' types to be compatible. Sam Owre gave a good justification of PVS's treatment of subtyping for functions on the main PVS list in April. I've quoted it below. In the theory you showed, you can eliminate the unprovable TCCs by writing the definition of f as f: [(q) -> nat] = restrict(LAMBDA (x: (p)): x - 1) As Sam points out, `restrict' is a conversion. I don't quite understand the circumstances under which conversions are automatically applied, so I'm not sure why it must be used explicitly here. - Darrell Sam Owre writes: > We chose not to use contravariance in order to keep equality simple; > equals can always be substituted for equals without worrying about the > type of the equalities (assuming everything is well-formed to begin > with). Thus in > > ex: THEORY > BEGIN > i: VAR int > n: VAR nat > abs(i): nat = IF i < 0 THEN -i ELSE i ENDIF > idint(i): int = i > idnat(n): nat = n > abs_is_id: FORMULA > idnat = abs and idnat = idint IMPLIES idint = abs > END ex > > the formula abs_is_id should not be provable. In PVS, the above does > not typecheck as given because [nat -> nat] and [int -> nat] are not > compatible types, i.e., they do not share a common supertype. Not > having contravariance can be inconvenient in many cases, so we added > conversions to the language. The prelude defines the restrict > operator as follows: > > restrict [T: TYPE, S: TYPE FROM T, R: TYPE]: THEORY > BEGIN > f: VAR [T -> R] > s: VAR S > restrict(f)(s): R = f(s) > CONVERSION restrict > END restrict > > and given f:[int->int], G[[nat->int]->bool], G(f) is automatically > transformed by the typechecker to G(restrict[int,nat,int](f)). > We also define an extension operator: > > extend [T: TYPE, S: TYPE FROM T, R: TYPE, d: R]: THEORY > BEGIN > f: VAR [S -> R] > t: VAR T > extend(f)(t): R = IF S_pred(t) THEN f(t) ELSE d ENDIF > END extend > > In this case, we can't easily make extend a conversion, as the > typechecker will never be able to derive the default value d. This > default is similar to using 0 or 9999 as a default representing > invalid values in a program or database. In one case that occurs > frequently, however, there is a good default value. This is when > dealing with predicates (which are also sets in PVS), where the > range type is boolean. By using FALSE for the default, as is done > in the prelude, then given s:pred[nat], P[pred[int] -> int], the > term P(s) is transformed to P(extend[int,nat,bool,false](s)). This > allows a set of nats to be viewed as a set of ints. > > In the abs_is_id example, the restrict operator is automatically > applied, and if you try to prove the formula you will see > > abs_is_id : > > {-1} idnat = restrict(abs) > {-2} idnat = restrict(idint) > |------- > {1} idint = abs >

**References**:**subtyping problem***From:*Jean-Paul BODEVEIX <bodeveix@irit.fr>

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