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

Re: [PVS-Help] Prooflite scripts being ignored?



Ben, 
The problem is that you have the proof script:

%|- *_TCC* : PROOF 
                   
                   
  %|-   (model-check)
                   
                   
  %|- QED          
                   
                   

after 

%|- Sqrt_x_2_y_2_TCC2 : PROOF
                   
                   
  %|-   (grind)    
                   
                   
  %|- QED          
                   
                   

Since *_TCC* matches Sqrt_x_2_y_2_TCC2, it rewrites the proof of
Sqrt_x_2_y_2_TCC2 to (moel-check). To solve this problem, put the most
greedy proof script, i.e., *_TCC*, before any other proof script.

Let me know if this solves your problem,

Cesar 





On 7/21/14 4:25 PM, "Ben Hocking" <benjaminhocking@xxxxxxxxx> wrote:

>I'm running PVS Version 6.0, and have the following (auto-generated)
>theory:
>distance3: 
>THEORY
>BEGIN
>IMPORTING reals@sqrt
>
>
>% Type of output  
>                  
>                  
>out_type:
>TYPE = [#
>                   f_result: real
>                  #]
>
>
>% Type of system state
>                  
>                  
>sys_type:
>TYPE = [#
>                   f_output: out_type
>                  #]
>
>
>result(p_Sqrt_x_2_y_2: real): real
>=
>  p_Sqrt_x_2_y_2
>
>
>Sqrt_x_2_y_2(p_x: real, p_y: real): real
>=
>  sqrt((p_x) 
>^ 2 + (p_y) 
>^ 2)
>
>
>% Initialize output
>                  
>                  
>prepare_output(p_result: real): out_type=
>  (#
>    f_result 
>:= p_result
>   #)
>
>
>% Initialize system state
>                  
>                  
>init: sys_type=
>  (#
>    f_output 
>:= prepare_output(0)
>   #)
>
>
>% Whole system run, this can only be called after INIT and inputs setting
>                  
>                  
>run(p_sys: sys_type, p_x: real, p_y: real): sys_type=
>  
>LET v_Sqrt_x_2_y_2: real = Sqrt_x_2_y_2(p_x, p_y)
>IN
>  
>LET v_result: real = result(v_Sqrt_x_2_y_2)
>IN
>  (#
>    f_output 
>:= prepare_output(v_result)
>   #)
>
>
>  %|- Sqrt_x_2_y_2_TCC1 : PROOF
>                  
>                  
>  %|-   (model-check)
>                  
>                  
>  %|- QED         
>                  
>                  
>
>
>  %|- Sqrt_x_2_y_2_TCC2 : PROOF
>                  
>                  
>  %|-   (grind)   
>                  
>                  
>  %|- QED         
>                  
>                  
>
>
>  %|- *_TCC* : PROOF
>                  
>                  
>  %|-   (model-check)
>                  
>                  
>  %|- QED         
>                  
>                  
>
>
>  %|- *int*_TCC* : PROOF
>                  
>                  
>  %|-   (grind)   
>                  
>                  
>  %|- QED 
>
>
>
>END distance3
>
>
>
>Running proveit does not execute my Prooflite scripts:
>▶ proveit -i -s distance3
>Processing ./distance3.pvs. Writing output to file ./distance3.summary
>Proving chain of imported theories
> Proof summary for theory distance3
>    Sqrt_x_2_y_2_TCC2.....................unfinished
>[shostak](0.09 s)
>    Theory totals: 2 formulas, 2 attempted, 1 succeeded (0.09 s)
>Grand Totals: 2 proofs, 2 attempted, 1 succeeded (0.09 s)
>
>
>
>I can verify this by entering PVS and choosing to re-run the proof for
>Sqrt_x_2_y_2_TCC2:
>Sqrt_x_2_y_2_TCC2 :
>
>
>  |-------
>{1}   FORALL (p_x, p_y: real): (p_x) ^ 2 + (p_y) ^ 2 >= 0
>
>
>Rerunning step: (subtype-tcc)
>
>…
>…
>{-1}  real_pred(p_x!1)
>{-2}  real_pred(p_y!1)
>  |-------
>{1}   expt(p_x!1, 2) + expt(p_y!1, 2) >= 0
>
>
>Rule?
>
>
>
>If I at this point issue the command
>(grind), I get the QED that I would expect.
>
>
>Am I doing something wrong, or is this a known issue? I could be wrong,
>but I think it used to work in PVS Version 5.
>
>
>Best Regards
>Ben Hocking
>benjaminhocking@xxxxxxxxx
>
>
>
>
>