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

PVS Bug 712


Synopsis:        Type of function updates
Severity:        serious
Priority:        medium
Responsible:     owre
State:           analyzed
Class:           sw-bug
Arrival-Date:    Mon Aug 26 10:55:01 2002
Originator:      Bruno Dutertre
Organization:    sdl.sri.com
Release:         PVS 3.0
Environment: 
 System:          
 Architecture: 

Description: 
  Sam,
  
  PVS3 does not typecheck expressions of
  the form f WITH [(x) := a] in the same
  way as PVS2.4. This happens when the
  types are as in this example:
  
  test : THEORY
  
     BEGIN
  
     T: TYPE+
     U: TYPE+ FROM T
  
     a: T
     f: [nat -> U]
     g: [nat -> T] = f WITH [(0) := a]
  
     END test
  
  This used to typecheck fine. Now,
  there is an unprovable TCC:
  
  g_TCC1: OBLIGATION U_pred(a);
  
  This can be solved with a type coercion,
  so it's not clear whether that's a bug,
  but just in case.
  
  Bruno
  
  

How-To-Repeat: 

Fix: 
Seems to have already been fixed for bug # 698
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools