Representing Component States in Higher-Order Logic
Sidi Ould Ehmety, Lawrence Charles Paulson, Lawrence Charles Paulson · 2002
Abstract. Component states can be formalized in higher-order logic as (1) functions from variables to values and (2) records, among other possibilities. Variable-to-value maps are natural, but they yield weak typing and restrict the user to a predefined value space. Record types define component signatures and properties need to be transferred between the various signatures. The method yields strong typing, but transferring properties requires an elaborate theory and not all properties can be transferred. The paper reports experiments with a third method: the state is represented by an abstract type. The method is described and contrasted with respect to the others. 1