# Verification of Control System Runtime Using an Executable Semantic Model +
## 4 Denotations of Instructions
### Adding and Division Functions
Its task is to return from a user subroutine by retrieving the values of the code and data registers stored on the \(cs\) and \(ds\) stacks, respectively, and setting them as the current values of the code and data registers. This procedure retrieves the value of the code register \(clbl_{1}\), stored earlier on the code stack by the CALB procedure, and the updated code stack \(cstk\) after using the function \(Pop\). Similarly, it retrieves the value of the data register \(dr_{1}\) and the new data stack \(dstk\). As a result, the procedure returns a new state, which is updated by utilizing the retrieved values representing the new code and stacks, code register, and data register:  
\[ \begin{split}&\mathcal{C}[\texttt{RETURN}]=\lambda s.\\ &(cm,dm,cs,ds,cr,dr,ex,flg):=\ s\\ &(clbl_{1},cstk):=\ Pop(cs)\\ &(dr_{1},dstk):=\ Pop(ds)\\ & s_{1}:=\ (cm,dm,cstk,dstk,clbl_{1},dr_{1},flg)\\ & s_{1}\\ \end{split}  \tag{27}\]  
\[ \begin{split}&\mathcal{C}[\texttt{GAWR:dst:src:size:idx}]=\lambda s.\\ &(cm,dm,cs,ds,cr,dr,ex,flg):=\ s\\ & dst:=\ GetAddress(cr,cm)\\ & cr_{1}:=\ cr\oplus AddressSize\\ & src:=\ GetAddress(cr_{1},cm)\\ & srcaddr:=\ dr\oplus src\\ & cr_{2}:=\ cr_{1}\oplus AddressSize\\ & size:=\ GetAddress(cr_{2},cm)\\ & sizeaddr:=\ dr\oplus size\\ & sizeval:=\ WordOf(Get2 BMem(sizeaddr,dm))\\ & cr_{3}:=\ cr_{2}\oplus AddressSize\\ & idx:=\ GetAddress(cr_{3},cm)\\ & idxaddr:=\ dr\oplus idx\\ & idxval:=\ WordOf(Get2 BMem(idxaddr,dm))\\ & cr_{4}:=\ cr_{3}\oplus AddressSize\\ & resultaddr:=\ dst\oplus idxval\otimes sizeval\\ & num:=\ MemMove(dm,resultaddr,dm,sraddr,sizeof)\\ & s_{1}:=\ (cm,um,cs,ds,cr_{4},dr,flg)\\ & s_{1}\\ \end{split} \]\[\begin{split}&\mathcal{C}[\texttt{CEAC:idx:lobase:hilevel}]=\lambda s.\\ &(cm,dm,cs,ds,cr,dr,ex,flg):=\ s\\ & idx:=\ GetAddress(cr,cm)\\ & idxaddr:=\ dr\oplus idx\\ & idxval:=\ IntOf(Get2 BMem(idxaddr,dm))\\ & cr_{1}:=\ cr\oplus AddressSize\\ & lobase:=\ GetAddress(cr_{1},cm)\\ & lobaseaddr:=\ dr\oplus lobase\\ & lobaseval:=\ IntOf(Get2 BMem(lobaseaddr,dm))\\ & cr_{2}:=\ cr\oplus AddressSize\\ & hilevel:=\ GetAddress(cr_{2},cm)\\ & hileveladdr:=\ dr\oplus hi\\ & hilevelval:=\ IntOf(Get2 BMem(hileveladdr,dm))\\ & lozero:=\ idxval\ominus\ lobaseval\\ & num:=\ Upd2 BMem(idxaddr,dm,FromInt(lozero))\\ & s_{1}:=\ \texttt{match}\ lozero\ \geq 0\ \& lozero\ \leq\ \mathit{lievelval}\ \texttt{with}\\ &\ |\ \texttt{true}\rightarrow(cm,um,cs,ds,cr3,dr,ex,flg)\\ &|\ \texttt{false}\rightarrow(ps,e0):=\ ex\\ & e0_{1}:=\ (\sigma_{3},\ \texttt{OUT}_{OF}\_{BOUNDS}\_{EXC})\\ & ex_{1}:=\ (ps,e0_{1})\\ & nflg:=\ SetFlag(flg,OUT\_OF\_BOUNDS\_EXC)\\ &\  
code stack, data stack, code register, data register, and flags. It also involves the exception state, consisting of the protected stack and the exception object. The code register and data register are variables of type Address, while the Flags type is an alias for uint16. A set of IEC 61131-3 data type aliases has also been defined as the discriminated union ValueType. **Listing 1. **\(\mathbb{F}^{4}\) definitions of the model domains. type Address = uint32  
type Storage = byte array type Memory = (Address * Storage) -> byte type Stack = Address list type Flags = uint16  
type ProtEntry = (Address * Address * Address * Address) type ProtStack = ProtEntry list type ExcObj = Address type ExcState = ProtStack * ExcObj  
type State = (Storage * Storage * Stack * Stack * Address * Address * ExcState * Flags)  
type ValueType = | BOOL of bool | BYTE of byte | WORD of uint16 | DWORD of uint32 | LWORD of uint64 | SINT of byte | INT of int16 | DINT of int32 | LINT of int64 | REAL of float32 | LREAL of float | TIME of uint32