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

PVS Bug 1045


Synopsis:        [PVS Bug] Formal parameter conversion
Severity:        serious
Priority:        medium
Responsible:     owre
State:           open
Class:           sw-bug
Arrival-Date:    Wed Feb 04 14:10:00 -0800 2009
Originator:      Natarajan Shankar
Release:         PVS 4.2
Organization:    csl.sri.com
Environment: 
 System:          
 Architecture: 

Description: 
  
  ALC_bug  [D, C, R : TYPE,
            atom_meaning: [C -> set[D]],
            roll_meaning: [R -> set[[D, D]]]]
  		: THEORY
  
    BEGIN
  
     
  
     CONVERSION atom_meaning
     CONVERSION roll_meaning
  
     i, j, k: VAR C
     a, b, c: VAR set[D]
     p, q, r: VAR R
  
     atom(i): set[D] = i;
  
     OR(a, b): set[D] = union(a, b);
  
     NOT(a): set[D] = complement(a);
  
     AND(a, b): set[D] = intersection(a, b);
  
     EXIST(p, a): set[D] = preimage(p, a)
  
     EVERY(p, a): set[D] = precondition(p, a)
  
  
  
    END ALC_bug

How-To-Repeat: 

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