Closed DavePearce closed 2 years ago
In order to describe the semantics of bytecode instructions in Whiley, it would be useful to have the array and record update operators. For example:
property ldc(int[] regs, int rd, int val) -> (int[] regs): regs[rd:=val]
In order to describe the semantics of bytecode instructions in Whiley, it would be useful to have the array and record update operators. For example: