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

[PVS-Help] Prooflite scripts being ignored?



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