Lab for Automated Reasoning and Analysis LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
sav08:immutable_abstract_data_types [2008/05/28 05:01]
vkuncak
sav08:immutable_abstract_data_types [2008/05/28 05:03] (current)
vkuncak
Line 34: Line 34:
 **Value construction consequence:​** Let $v$ be a value of an immutable ADT computed by a (potentially mutable) function in a type safe language. ​ Then there exists a finite expression tree whose nodes are operations of ADT and whose leaves are either nullary operations of ADT or non-ADT values, such that this expression tree evaluates to value $v$. **Value construction consequence:​** Let $v$ be a value of an immutable ADT computed by a (potentially mutable) function in a type safe language. ​ Then there exists a finite expression tree whose nodes are operations of ADT and whose leaves are either nullary operations of ADT or non-ADT values, such that this expression tree evaluates to value $v$.
  
-Note that this consequence does not rely on any properties of the function computing $v$.  The function could be arbitrarily complex. ​ The expression tree is the part of the computation that is relevant for computing $v$ (for non-ADT values, it need not keep track how they are computed).+Note that this consequence does not rely on any properties of the function computing $v$.  The function could be arbitrarily complex, and need not terminate for all inputs, as long as we consider an evaluation that computed $v$.  The expression tree is the part of the computation that is relevant for computing $v$ (for non-ADT values, it need not keep track how they are computed).
  
 In the previous example, we are sure that all natSet values computed in any code that uses the ADT are obtained by starting from empty and applying operations insert,​remove,​union. In the previous example, we are sure that all natSet values computed in any code that uses the ADT are obtained by starting from empty and applying operations insert,​remove,​union.
  
 
sav08/immutable_abstract_data_types.txt · Last modified: 2008/05/28 05:03 by vkuncak
 
© EPFL 2018 - Legal notice