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

*To*: pvs-help@csl.sri.com*Subject*: assumptions/obligations*From*: rmb@dcs.gla.ac.uk*Date*: Thu, 21 May 1998 16:55:49 +0100

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.

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