Tools for automatically extracting the conditions for which a program is correct with respect to a precondition and postcondition can make proving program correctness easier. We build a HOL-based tool that uses weakest preconditions and semantically derived rules to prove correctness theorems with the verification conditions as assumptions. The rules include two new rules for calculating loop preconditions and recursion correctness while taking specification variables into consideration. The programming language has (recursive) procedures, and both demonic and angelic nondeterminism, which can be used to model interaction. Program variables can be of arbitrary types. Programs with procedures are handled modularly, and proved facts about individual procedures are stored in a database available to all programs.