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

PVS Bug 679


Synopsis:        Components not available in record definitions
Severity:        serious
Priority:        medium
Responsible:     owre
State:           open
Class:           sw-bug
Arrival-Date:    Tue Jul  9 11:05:01 2002
Originator:      Christoph Berg
Organization:    cs.uni-sb.de
Release:         PVS 2.4
Environment: 
 System:          
 Architecture: 

Description: 
  rec_depend: theory
  begin
  
    type1: TYPE = [# a: int, b: int #]
  
    %% in the following record type definition, the component 'a'
    %% is available in successive component type definitions:
  
    type2: TYPE = [# a: int, b: {x: int | x = a} #]
  
    %% it would be nice if PVS allowed the same for record definitions.
  
    %% the next definition yields the error message:
    %% Expecting an expression
    %% No resolution for a
  
    update_b(x: type1): type2 = (# a := x`a, b := a #)
  
    %% this one is ok (but we have to write x`a in place of a):
  
    update_b(x: type1): type2 = (# a := x`a, b := x`a #)
  
  end rec_depend
  
  -- 
  cb@cs.uni-sb.de, http://www-wjp.cs.uni-sb.de/~cb/
  Office +49/681/302-4129, Fax -4290, Home +49/681/9657944
  Computer Science Dept., Universität des Saarlandes, Saarbrücken
  

How-To-Repeat: 

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