ϵ">]>
Literature.
[1] J. Komara. Specification and Verification of Programs. Downloadable lecture notes available through the web page of the course.
[2] J. Komara and P. J. Voda. Metamathematics of Computer Programming. 2001.
[CL] Syntax. Identifier conventions:
Variable identifier. A string of lower case letters possibly followed by one or two digits as indices. Examples: , , , .
Function identifier. An alpha-numeric string starting with a capital letter and containing lower case letters, digits, and underline symbols '_'. Examples: , , , .
Square function. The next component contains the explicit definition of the function which yields the square of the number .
Sum of two squares. Write an explicit definition of the binary function which yields the sum of the squares and .
Hint. Press the Ins/Del button on the right.
Minimum. The binary function returns the smaller of its two arguments:
The following component contains an explicit clausal definition of the minimum function.
[CL] Remark. Here is an example of syntactically incorrect definition of the same function:
This is because the first application of the minimum function is syntactically different from the second . They should be identical as it is in the previous definition.
Summation. The following component contains a primitive recursive definition of the summation function :