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

*To*: yechiel@CS.Technion.AC.IL*Subject*: Re: What have I missed ? (a proof failed)*From*: Dave Stringer-Calvert <dave_sc@csl.sri.com>*Date*: Wed, 6 May 1998 09:35:20 -0700*CC*: pvs-help@csl.sri.com*In-reply-to*: <199805061517.SAA01603@CS.Technion.AC.IL>(yechiel@CS.Technion.AC.IL)

Yechiel --- Your proof can be completed with the following commands: (grind) (use "equal_ax") (grind) Check the on-line help for the commands `use' and `lemma' for more information on what they do (i.e. "(help use)"). On another note, you have an unprovable type correctness condition (TCC) in your theory, as you declare a constant `e' of the parameter type: stack_0[T: TYPE]: THEORY BEGIN ... e : T % a constant ... END stack_0 % Existence TCC generated (line 9) for e: T % % May need to add an assuming clause to prove this. % untried e_TCC1: OBLIGATION (EXISTS (x: T): TRUE); As `T' is declared as `TYPE', it can be an *empty* type, and as such declaring a constant of that type would be unsound. You can eliminate this problem by changing the declaration to a nonempty type by using the keywords `TYPE+' or `NONEMPTY_TYPE', for example: stack_0 [T : NONEMPTY_TYPE] : THEORY BEGIN e : T END stack_0 The TCC is no longer generated in this case. Hope that helps, Dave -- Dr Dave Stringer-Calvert, Software Engineer, Computer Science Laboratory, SRI International, 333 Ravenswood Avenue, Menlo Park, CA 94025-3493, USA. Phone: (650) 859-3291 Fax: (650) 859-2844 Email: dave_sc@csl.sri.com

**References**:**What have I missed ? (a proof failed)***From:*yechiel@CS.Technion.AC.IL (Yechiel Kimchi)

- Prev by Date:
**Re: What have I missed ? (a proof failed)** - Next by Date:
**Re: What have I missed ? (a proof failed)** - Prev by thread:
**Re: What have I missed ? (a proof failed)** - Next by thread:
**Default Library paths** - Index(es):