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

*To*: rmb@dcs.gla.ac.uk*Subject*: Re: assumptions/obligations*From*: John Hoffman <hoffman@securecomputing.com>*Date*: Thu, 21 May 1998 12:50:15 -0500 (CDT)*Cc*: pvs-help@csl.sri.com*In-Reply-To*: <199805211555.QAA18076@ascension.dcs.gla.ac.uk> from "rmb@dcs.gla.ac.uk" at May 21, 98 04:55:49 pm

> In chunnel.pvs I have, for instance, a theory 'points' which > defines a type 'points_value' and an assumption on this type > 'points_ax'. In the theory 'Thedford_scenario' a constant 'mp' of > type 'points_value' is declared and instantiated. I thought that > this would then incur an obligation to prove the assumption > 'points_ax'. However, on doing a typecheck no such tcc occurs. Why > is this? Is there any other way to write this so that the relevant > tcc's occur? > > Richard. Assumptions require you to prove theorems on the formal parameters passed into a theory. That's not happening in your case. This is described in slightly more detail in the PVS language spec in section 6. Here's a way to define point_values so it generates your desired tcc's There's probably a slicker way to do it, but I think you'll get the idea. point_values: TYPE = ({(mpv : finseq[real] ) | length(mpv) >= 2 AND (FORALL (i: nat): member(i, {n: nat | n <= length(mpv) - 2}) IMPLIES seq(mpv)(i) > seq(mpv)(i + 1))}) cheers, John ==============================++==================== John Hoffman, PhD || Secure Computing Corporation || What do you want to 2675 Long Lake Road || read for, when you Roseville, MN 55113 || can watch TV? hoffman@securecomputing.com || Fax :(612)628-2701 || - Matilda's Father Phone:(612)628-2808 || ==============================++====================

**References**:**assumptions/obligations***From:*rmb@dcs.gla.ac.uk

- Prev by Date:
**assumptions/obligations** - Next by Date:
**problem on typechecking** - Prev by thread:
**assumptions/obligations** - Next by thread:
**Red Hat 5.0 libraries** - Index(es):