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

PVS Bug 490


Synopsis:        TYPE+ FROM leads to unprovable TCC
Severity:        serious
Priority:        medium
Responsible:     dave_sc (Dave Stringer-Calvert)
State:           analyzed
Class:           sw-bug
Arrival-Date:    Thu Sep 28 10:40:01 2000
Originator:      Holger PFEIFER
Organization:    ares.informatik.uni-ulm.de
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 
  Sam/Dave,
  
  for the IMPORTING clause in theory Th2 below the typechecker 
  (PVS Version 2.3 (patch level 1.2.2.36)) generates the unprovable TCC:
  
  	% Subtype TCC generated (at line 17, column 22) for  f
  	  % unfinished
  	IMP_Th1_TCC1: OBLIGATION FORALL (x1: D): S_pred(f(x1));
  
  I believe this TCC shouldn't be generated, and if I think it should read 
  
  	IMP_Th1_TCC1: OBLIGATION FORALL (x1: D): B_pred(f(x1));
  
  The TCC doesn't occur if I remove the + in the declaration of the type
  of S and change it to TYPE FROM R - very strange...
  
  Cheers,
  
  	- Holger
  
  
  Th1 [D : TYPE+,         % -- Domain type
       R : TYPE+,         % -- Range type
       S : TYPE+ FROM R,  % -- Subtype of range
       f : [D->S]         % -- function into subtype
      ] : THEORY
  BEGIN
  END Th1
  
  Th2 [D : TYPE+] : THEORY
  BEGIN
  
    A : TYPE+ = nat
    B : TYPE+ = A
  
    f(d:D): B = 0
  
    IMPORTING Th1[D,A,B,f]
  
  END Th2
  
  -- 
  --------------------------------------------------------------------
  Holger Pfeifer                           Tel.: +49 (0)731 / 50-24124
  Universität Ulm                           Fax: +49 (0)731 / 50-24119
  Abt. Künstliche Intelligenz         pfeifer@ki.informatik.uni-ulm.de
  D-89069 Ulm         http://www.informatik.uni-ulm.de/ki/pfeifer.html   
  --------------------------------------------------------------------

How-To-Repeat: 

Fix: 

 [davesc]
 Fixed in 2.3.1 - no TCCs are generated.

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