# Verification of Control System Runtime Using an Executable Semantic Model +
## 4 Denotations of Instructions
### Machine Instructions  
The semantic equations presented in Section 4 define the steps taken during the processing of individual instructions executed by the virtual machine but only for one particular data type. Most functions have multiple variants, largely due to the types of operands they accept. Some functions also have variants with different numbers of operands. The semantic models for different variants of functions differ only in the use of functions for memory read, memory write, and value interpretation. To avoid duplicating code and writing several similar functions performing the same operation but with slight modifications, generic functions are implemented to handle all variants of a given instruction. The discriminated union type ValueType is used (Listing 1) to represent the basic types. The ADD instruction, which performs the addition operation, has multiple variants for different numbers of operands (2 to 15) and different data types. The generic implementation of ADD is presented in Listing 6. The function accepts a parameter of type State, containing the current values of individual components describing the machine state. It also receives auxiliary functions as parameters, which handle data retrieval from memory (getBytes), their interpretation into the appropriate type (typeOf), type conversion into the appropriate byte representation (fromType), and data storage in memory (updBytes). Since ADD operates on different numbers of operands, an additional parameter count specifies how many operands are to be added. Initially, the address for storing the result is retrieved. Then, the operation retrieves a specified number of operands from the data memory based on the determined addresses and interprets them into the appropriate type using the interpretation function passed as a parameter. Finally, using the reduce function from the List module, each operand is matched to the appropriate ValueType union type to retrieve the value of each operand, after which the addition operation is performed on all operands. The resulting value is then stored in memory at the determined address raddr using the conversion function passed as a parameter. The function returns a new state containing the updated data memory after storing the result along with the current value of the code register crx. ```
letADD(state:State,getBytes:(Address+Storage)->'a,updBytes:(Address* Storage*'a)->Storage,typeOf:'a->ValueType,fromType:ValueType->'a,count:int)= let(cm,dm,cs,ds,cr,dr,ex,flg)=state letr=GetAddress(cr,cm) letraddr=dr+r letmutablecrx=cr+AddressSize letmutablelst=[] fori=1 tocountdo letopx=GetAddress(crx,cm) letopxaddr=dr+opx letopxvalue=typeOf(getBytes(opxaddr,dm)) lst<-opxvalue::lst crx<-crx+AddressSize printf$\"Op%A{i}:%A{opvvalue}\" letvalue=List.reduce(funaccel-> matchacc,elwith |SINTa,SINTb->SINT(a+b) |INTa,INTb->INT(a+b) |DINTa,DINTb->DINT(a+b) |LINTa,LINTb->LINT(a+b) |BYTEa,BYTEb->BYTE(a+b) |WORDa,WORDb->WORD(a+b) |DWORDa,DWORDb->DWORD(a+b) |LWORDa,LWORDb->LWORD(a+b) |REALa,REALb->REAL(a+b) |LREALa,LEALb->LREAL(a+b) |_->failwith\"Wrongata\" ) lst printfn$\"\
ADDresult:%A{value}\" (cm,updBytes(raddr,dm,fromType(value)),cs,ds,crx,dr,ex,flg)The DIV instruction is defined similarly as shown in Listing 7 with parameter decoding dropped for brevity. However, it includes an additional block to check for a bad divisor (i.e., when it equals zero). If such a condition is met, an exception object is created and the exception is raised.