Recursive Programs with Parameters

Now That We understand the semantics and verification of recursive procedures without parameters, we extend our study to the case of recursive procedures with parameters. The presentation follows the one of the last chapter. In Section 5.1 we introduce the syntax of recursive procedures with parameters. We deal here with the most common parameter mechanism, namely call-by-value. To properly capture its meaning we need to introduce a block statement that allows us to distinguish between local and global variables. In Section 5.2 we introduce the operational semantics that appropriately modifies the semantics of recursive procedures from the last chapter. The block statement is used to define the meaning of procedure calls. Then, in Section 5.3 we focus on program verification. The approach is a modification of the approach from the previous chapter, where the additional difficulty consists of a satisfactory treatment of parameters. Finally, as a case study, we consider in Section 5.5 the correctness of the

Quicksort

program.