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

PVS Bug 443


Synopsis:        TCC generation
Severity:        serious
Priority:        medium
Responsible:     dave_sc (Dave Stringer-Calvert)
State:           analyzed
Class:           sw-bug
Arrival-Date:    Fri Feb 25 00:40:01 2000
Originator:      Mamoun FILALI-AMINE
Organization:    irit.fr
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 
  The TCCs generated for function calls appearing as parameters of
  theories is not correct:
  The context is lost. However, if the parameters are expressed as single
  variables the
  context is actually transmitted  to the TCCs
  
  Release:         PVS 2.3
  
  yy[x1:nat]: THEORY
  BEGIN
    p: bool = true
  END yy
  
  xx: THEORY
  BEGIN
    IMPORTING yy
    u: nat
    g(x:upto(u)):nat = x
    xx: THEOREM
      FORALL (x:nat):  x<=u & p[g(x)]
  % Subtype TCC generated (at line 15, column 39) for  x
    % untried
  %xx_TCC1: OBLIGATION FORALL (x: nat): x <= u;
  %%%%%%%%%%%%%%%%%%%%%%% the context x <=u is lost
  %%%%%%%%%%%%%%%%%%%%%%%we should have: ... x<=u => x<=u
  END xx
  
  
  --
  Mamoun Filali
  filali@irit.fr
  Tel: (+33) 5 61 55 69 26 Fax (+33) 5 61 55 68 47
  IRIT Universite Paul Sabatier
  118 Route de Narbonne
  F-31062 Toulouse cedex
  France
  
  

How-To-Repeat: 

Fix: 

 [davesc, 7/17/01]
 Fixed in PVS 2.3.1 - doesn't generate the TCC any more as with the
 context included it's trivial.

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