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

*To*: TENEVA G Ms -NUCLEAR <galina.teneva@opg.com>*Subject*: Re: FW: PVS Problems*From*: Sam Owre <owre@csl.sri.com>*Date*: Wed, 02 Jan 2002 21:25:37 -0800*cc*: "'pvs-help@csl.sri.com'" <pvs-help@csl.sri.com>, owre@csl.sri.com*In-Reply-To*: Your message of "Wed, 02 Jan 2002 13:00:39 EST." <FA9026F241D3D411A04B00805FFE91C301CA930C@TORI>*Sender*: pvs-help-owner@csl.sri.com

Hi Galina, > I have two problems using the PVS, version 2.3, patch level 1.2.2.36. > 1) After proving the generated TCCs and the theorem (att. B029.pvs), I can > not view the TCCs i.e. if I the click on the "Viewing TCCs" and then on > "show-tccs", the content is empty and there is a message "parser error". > Take into account, please, that during the process of proving the TCCS or > the theorem, no error message appears. > As we don't have pvs e-mail working, I attached here the pvs files B029.pvs > and math_fun.pvs. The math_fun.pvs has to be typechecked (and so > math_fun.bin to be created) before running the B029.pvs. > The problem can be avoided if in the function: > AbstG_AbstA2D_HTPressure( > x: ARRAY[subrange(1,4) -> subrange(0,5119)]): t_SnrValAll = > LAMBDA(i:subrange(1,48)): > COND > ((39 <= i) & (i <= 42)) > -> AbstA2D(x((i - (39 - 1)))), > ELSE > -> epsilon(LAMBDA(randomVal:t_SnrValue): FALSE) > ENDCOND > the ELSE is replaced by NOT((39 <= i) & (i <= 42)). This problem has been fixed in the recently released PVS version 2.4. Please download it from the PVS home page. Your specification implicitly uses the K_conversion, which is now off by default, so you'll need to add the line CONVERSION K_conversion near the beginning of your spec. Unfortunately your spec exposes a bug in PVS 2.4, so you'll also need to load the following code (add it to your ~/.pvs.lisp file). (defmethod application-conversion-argument (arg (conv name-expr) vars) (let ((var1 (find-if #'(lambda (v) (tc-eq (type v) (domain (range (type conv))))) vars))) (if (some #'(lambda (ty) (and (funtype? (find-supertype ty)) (compatible? (domain (find-supertype ty)) (type var1)))) (ptypes arg)) (let ((ac (make-instance 'argument-conversion 'operator arg 'argument var1))) (typecheck* ac nil nil nil)) arg))) > 2) In the att. CIOB051.pvs, among the other input parameters there are > mk_SGLLcondIn and mk_SGLLcondOut. > The mk_SGLLcondIn is declared as a constant mk_SGLLcondIn: t_SGLLcondRange = > 2349, where t_SGLLcondRange is subrange(2349, 3239). > The mk_SGLLcondOut is declared as a variable: mk_SGLLcondOut: VAR {x: > t_SGLLcondRange | x < mk_SGLLcondIn}. > These two inputs are used in the function f_LogNLowForSGLLconditioning: > f_LogNLowForSGLLConditioning( > mk_SGLLcondIn: t_SGLLcondRange, > mk_SGLLcondOut: {x:t_SGLLcondRange | x < mk_SGLLcondIn}, > m_LogN: subrange(0,5119), > f_LogNLowForSGLLConditioning_s1: bool): bool = > COND > (m_LogN >= mk_SGLLcondIn) > -> FALSE , > ((mk_SGLLcondIn > m_LogN) & (m_LogN > mk_SGLLcondOut)) > -> f_LogNLowForSGLLConditioning_s1, > (mk_SGLLcondOut >= m_LogN) > -> TRUE > ENDCOND > As you can see, if mk_SGLLcondIn = 2349, then mk_SGLLcondOut has to be < > 2349 and as the data type of mk_SGLLcondOut is subrange(2349, 3239), there > is no x which can satisfied this condition. > In the process of proving this theorem, all tccs are proved and the theorem > is proved as well. > It is not the case, if in the function f_LogNLowForSGLLConditioning, for the > input parameter mk_SGLLcondOut, an explicit value for the input constant > mk_SGLLcondIn = 2349 is used: > ..... > f_LogNLowForSGLLConditioning( > mk_SGLLcondIn: t_SGLLcondRange, > mk_SGLLcondOut: {x:t_SGLLcondRange | x < 2349}, > m_LogN: subrange(0,5119), > f_LogNLowForSGLLConditioning_s1: bool): bool = ... > Then a type check error "Subtype TCC for mk_SGLLcondOut simplifies to FALSE" > appears. As these two versions of the theorem look identical to me, why a > typecheck error should appear in one of the cases? Actually I would expect > that the same typecheck error will appear in both cases, as there is no x of > data type t_SGLLcondRange, which is < 2349. > Attached to this e-mail is the pvs file CIOB051.pvs. It has to be run from > the same directory where math_fun.bin is(math_fun.bin is automatically > produced if math_fun.pvs is typechecked). The issue here is one of empty types. These make sense mathematically, and are legal in PVS, as long as no constant is declared to be of that type, i.e., as long as only variables range over the type. Parameters in a function definition are always variables, so they cause no problem even if their type is empty, but there is then the issue that one may be defining the empty function, which is perfectly OK mathematically, but often not what was intended. One way to ensure that a function has a nontrivial definition is to demonstrate that its domain is nonempty. This usually happens as a side effect of application, unless the function is only ever applied variables. This is what is happening in your case: f_LogNLowForSGLLConditioning is invoked in vb_B051_1 and vb_B051_2 with second argument mk_SGLLcondOut, which is declared as a variable. If you are concerned that some of your function definitions might inadvertently be empty, I suggest you augment each of these definitions with a lemma that asserts their domain is nonempty. Regards, Sam Owre

**References**:**FW: PVS Problems***From:*TENEVA G Ms -NUCLEAR <galina.teneva@opg.com>

- Prev by Date:
**FW: PVS Problems** - Next by Date:
**Latex printing. a problem.** - Prev by thread:
**FW: PVS Problems** - Next by thread:
**Category Theory** - Index(es):