Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools

PVS Bug 878


Synopsis:        [PVS-Help] nonempty type tcc
Severity:        serious
Priority:        medium
Responsible:     owre (Sam Owre)
State:           analyzed
Class:           sw-bug
Arrival-Date:    Thu Dec  2 22:25:00 2004
Originator:      robert
Organization:    itee.uq.edu.au
Release:         PVS 3.2
Environment: 
 System:          
 Architecture: 

Description: 
  
  I've just changed to version 3.2 and a problem has cropped up.
  
  I have a theory
  
  proc: THEORY
  begin
      PROC: TYPE+
  end proc
  
  I import this theory via library, eg, 
  
  sq_abstract: THEORY
  BEGIN
  	
  	lib: LIBRARY = "whatever"
  
  	importing lib@proc
  
  	.....
  
  	pp: PROC
  
  	.....
  end sq_abstract
  
  The type checker generates the tcc 
  
  % Existence TCC generated (at line 97, column 1) for  pp: PROC
    % unfinished
  pp_TCC1: OBLIGATION EXISTS (x: PROC): TRUE;
  
  This isn't proved when I use M-x prove-tccs-theory (ie, using (tcc)
  or (grind)).
  
  I introduced a theorem identical to pp_TCC1 in theory proc and was able 
  to prove it straight away using (grind).
  
  How can I prove the tcc obligation?
  
  Thanks,
  Rob

How-To-Repeat: 

Fix: 
Added restore-object* (nonempty-type-decl) to set the type-value to
nonempty

(defmethod restore-object* :around ((obj nonempty-type-decl))
  (call-next-method)
  (set-nonempty-type (type-value obj)))
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools