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

Help!




Hello

I have just started using PVS and I am having some trouble discharging
some of the proof obligations for termination TCCs.
If you can help me out with them, I'd be tremendously grateful(see below).

Also, there are some questions that I'd like to ask.

1) In general, how do you discharge such proof obligations as termination TCCs.
I tried M x tcp but it doesnt work always.
Also, in our of the literature that is found on the SRI website(re:pvs), it suggested
using the strategy (tcc), which I tried, to discharge some of the proof obligations
for the termination TCCs(see below), but I got an error msg saying this:

Found VAR when expecting
  opsym, (, (#, [|, (:, identifier, IF, TRUE, FALSE, [||], !STRING!, !NUMBER!, LAMBDA, FORALL, EXISTS, {, LET, CASES, COND, or TABLE
  
What is VAR ? and what does this error msg mean ?

2) How about existence TCCs

Many thanks

Arshad

______________________________________________________________________________
1.
% Termination TCC generated (at line 148, column 6) for  updating_state
  % unfinished
updating_state_TCC1: OBLIGATION
  FORALL (rest: list[variable], var_1: variable, updated_val: value_list, updated_var: list_of_vars):
    updated_var = cons(var_1, rest) AND updated_val = null IMPLIES length(rest) < length(updated_var);

2.
% Subtype TCC generated (at line 151, column 31) for  updated_val
% unfinished
updating_state_TCC2: OBLIGATION
  FORALL (rest: list[variable], var_1: variable, updated_val: value_list, updated_var: list_of_vars):
    updated_var = cons[variable](var_1, rest) AND NOT updated_val = null[value] IMPLIES cons?[value](updated_val);

3.
% Termination TCC generated (at line 151, column 6) for  updating_state
  % unfinished
updating_state_TCC3: OBLIGATION
  FORALL (rest: list[variable], var_1: variable, updated_val: value_list, updated_var: list_of_vars):
    updated_var = cons(var_1, rest) AND NOT updated_val = null IMPLIES length(rest) < length(updated_var);

This is the part of the spec that gave rise to the above TCCs.
%Else, each variable is updated with some values.
updating_state(updated_var	: list_of_vars,
	       updated_val	: value_list,	 
	       start_state 	: object_state): RECURSIVE object_state =
	CASES updated_var OF
		null			: start_state,
		cons(var_1, rest)	: IF   	updated_val = null THEN 
						updating_state(rest, null, start_state) WITH [(var_1) := null_value]
						
					  ELSE 
						updating_state(rest, cdr(updated_val), start_state) WITH [(var_1) := car(updated_val)]
						
					  ENDIF
	ENDCASES
	MEASURE length(updated_var)


******************************************************************************
Arshad Jhumka					Ph   : +46 31 772 5223
Dept of Computer Engineering			fax  : +46 31 772 3663
Chalmers University				email: arshad@ce.chalmers.se
Goteborg, SWEDEN
******************************************************************************