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

Help with TCCs



Hello,

I am trying to develop a theory where I am manipulating real and natural
numbers. I am having difficulties in discharging these TCCs obligations.
Could some one assist me in resolving this problem...

I am enclosing both the pvs and tccs files for your reference.

Thanks in advance.

Nikhil Varma

--------------------------PVS file ----------------
test  : THEORY

  BEGIN
   NatNum : posnat
   ID: TYPE = posnat
   NZTR: TYPE ={ RealNum: real | RealNum >0 }
   ZTR: TYPE ={RealNum: real | RealNum >=0 } containing 0
   n: VAR ID
   n1:VAR NZTR
   n2:VAR ZTR

   % multiplying Zero_Real + PosInteger* NonZeroReal should give zero_real type
   Mult (n,n1,n2): ZTR = n2 + n * n1

  % Dividing Pos integer with non zero real should give zero real
  Division(n,n1): ZTR = n/n1

 END test


----------------------TCCS generated----------
% Subtype TCC generated (at line 13, column 25) for  n2 + n * n1
    % expected type  ZTR
  % unfinished
Mult_TCC1: OBLIGATION FORALL (n: ID, n1: NZTR, n2: ZTR): n2 + n * n1 >= 0;

% Subtype TCC generated (at line 16, column 26) for  n1
    % expected type  nzreal
  % proved - complete
Division_TCC1: OBLIGATION FORALL (n1: NZTR): n1 /= 0;

% Subtype TCC generated (at line 16, column 24) for  n / n1
    % expected type  ZTR
  % unfinished
Division_TCC2: OBLIGATION FORALL (n: ID, n1: NZTR): n / n1 >= 0;