Classes and Objects Sample Clauses

Classes and Objects. ‌ Class processes encapsulate actions corresponding to the operations and threads of the corresponding VDM-RT class. Object processes will effectively create copies of their corresponding class process, but with an allocated object name. In our semantics we do not directly consider static instance variables and functions, which can be represented by similar constructs in CML. We assume that each class can be allocated a unique name represented by meta-tag ‹Classk›. Additionally, each object process of a particular class maintains its own central state. The various threads running within the class’s context copy and synchronise with this state using the channels getState-‹Classk› and syncState-‹Classk›. A semantic mapping for a typical class process is shown in Figure 8. The generated class process is parameteric over an object name objId that will be given when the class is instantiated. The state of the class, that is, the collection m of instance variables, is represented by the record type State-‹Classk› where ‹▇▇▇▇▇› is the instance variable name, and ‹ATm› its type. Thus the class process, VrtClass-‹Classk› has a state variable this of the state type, with initial values taken from the instance variable initial values ‹iai›. The state variable upd records the updates that have been made to the state as a total function on an existing state. It can then be applied to the central state when a thread needs to synchronise. · · · We assume there are n operations, named ‹Op1› ‹Opn›, with operation bodies ‹Op1Body› · · · ‹OpnBody›, respectively, which are encoded by respective actions that encode their thread behaviour. Additionally a class can optionally have a thread action, Thread, whose semantics will be described in the next section. The StateMgr action manages the central state for the class stored in state variable this. It can send the current central state to another action using the getState-‹Classk› channel, and can synchronise the state with an action using the syncState-‹Classk›. In the latter case the state manager updates the value of this by applying the update function to it. The main action of the process inter- leaves the operation and thread actions, and composes them with the state manager. The state manipulation channels are then hidden to ensure that state updates occur urgently: the clock cannot advance whilst a pending state update remains. We now describe the operation actions in more detail. Each operation action first waits for a ...