# Verification of Control System Runtime Using an Executable Semantic Model +
## 4 Denotations of Instructions
### Adding and Division Functions  
The ADD instruction with two INT operands referenced in Section 3.6 can be represented with the denotational Equation (18):  
\begin{table}
\begin{tabular}{c c c} \hline \hline
**Mnemonic** & **Meaning** & **Operator** \\ \hline NEG & Negation & - (unary) \\ AND & Logical and & \& \\ GT, GE & Greater, Greater or equal & \textgreater{}, \textgreater{}= \\ LT, LE & Less, Less or equal & \textless{}=, \textless{} \\ EQ, NE & Equal, Not equal & \textless{}=, \textless{}> \\ MUL, DIV & Multiplication, Division & \textless{}, / \\ ADD, SUB & Addition, Subtraction & +, - (arithmetic) \\ EXPT & Power & \(\mathbf{\mathbf{\mathbf{\mathbf{\mathbf{\mathbf{\mathbf{\mathbf{\mathbf{\mathbf{\mathbf{\mathbf{\mathbf{\mathbf{\  
\[ \begin{split}&\mathcal{C}[\texttt{ADD:INT:r:op1:op2}]=\lambda s.\\ &(cm,dm,cs,ds,cr,dr,ex,flg):=\ s\\ & r:=\ GetAddress(cr,cm)\\ & raddr:=\ dr\oplus r\\ & cr_{1}:=\ cr\oplus AddressSize\\ & op1:=\ GetAddress(cr_{1},cm)\\ & op1 addr:=\ dr\oplus op1\\ & cr_{2}:=\ cr_{1}\oplus AddressSize\\ & op2:=\ GetAddress(cr_{2},cm)\\ & op2 addr:=\ dr\oplus op2\\ & cr_{3}:=\ cr_{2}\oplus AddressSize\\ & sv:=\ IntOf(Get2 BMem(op1 addr,dm))\oplus IntOf(Get2 BMem(op2 addr,dm))\\ & s_{1}:=\ (cm,Upd2 BMem(addr,dm,FromInt(sv)),cs,ds,cr_{3},dr,flg)\\ & s_{1}\end{split}  \tag{18}\]  
Splitting the current state \(s\) into components \((cm,dm,cs,ds,cr,dr,flg)\) through unification is the first operation in the equation. A call to a particular function \(\mathcal{C}\) by universal \(\mathcal{U}\) is performed with the code register \(cr\) pointing to the first operand (\(cr_{2}\) in (17)). The first operand of the ADD instruction refers to the addition result. Its address is acquired from the code memory \(cm\) and stored in \(r\) by:  
\[r:=\ GetAddress(cr,cm) \tag{19}\]  
However, since the operand may be a local variable of a subprogram, the value \(r\) means a relative address counting from the current value of database register \(dr\), set during the subprogram call. Therefore, the absolute address of the local variable in data memory is obtained by:  
\[raddr:=\ dr\oplus r \tag{20}\]  
In the case of a global variable, the value \(dr\) is zero, so \(raddr\) equals \(r\). Since the ADD instruction has other operands, the code register \(cr\) is later incremented to point out to the next memory location:  
\[cr_{1}:=\ cr\oplus AddressSize \tag{21}\]  
The next two operands \(op1\) and \(op2\) are processed similarly. After all the operands are available, addition may take place. The variable values to be added are read out from data memory \(dm\) and interpreted as INTs (Sections 3.4 and 3.5), using the expression:  
\[IntOf(Get2 BMem(operandaddr,dm)) \tag{22}\]  
The result of the addition \(\oplus\) is stored in \(sv\). Then, the new state \(s_{1}\) is constructed as the tuple:  
\[s_{1}:=\ (cm,Upd2 BMem(raddr,dm,FromInt(sv)),cs,ds,cr_{3},dr,flg) \tag{23}\]\[\begin{split}&\mathcal{C}[\texttt{DIV:INT:r:op1:op2}]=\lambda s.\\ &(cm,dm,cs,ds,cr,dr,ex,flg):=\ s\\ & r:=\ GetAddress(cr,cm)\\ & raddr:=\ dr\oplus r\\ & cr_{1}:=\ cr\oplus AddressSize\\ & op1:=\ GetAddress(cr_{1},cm)\\ & op1 addr:=\ dr\oplus op1\\ & cr_{2}:=\ cr_{1}\oplus AddressSize\\ & op2:=\ GetAddress(cr_{2},cm)\\ & op2 addr:=\ dr\oplus op2\\ & cr_{3}:=\ cr_{2}\oplus AddressSize\\ & divvisor:=\ IntOf(Get2 BMem(op2 addr,dm))\\ &\textbf{match}\ divisor\ \textbf{with}\\ &\mid\ 0\to ex:=\ (cr_{3},DIV\_BY\_Zero\_EXC)\\ &\quad\  
\[ \begin{split}&\mathcal{C}[\texttt{CALB:inst:clbl}]=\lambda s.\\ &(cm,dm,cs,ds,cr,dr,ex,flg):=\ s\\ & inst:=\ GetAddress(cr,cm)\\ & instaddr:=\ dr\oplus inst\\ & cr_{1}:=\ cr\oplus AddressSize\\ & clbl:=\ GetAddress(cr_{1},cm)\\ & cr_{2}:=\ cr_{1}\oplus AddressSize\\ & s_{1}:=\ (cm,dm,Push(cs,cr_{2}),Push(ds,dr),clbl,instaddr,flg)\\ & s_{1}\\ \end{split}  \tag{26}\]  
In Equation (27), the denotation of the RETURN procedure is provided.