The PVS specification language extends simply typed higher-order logic with a number of useful features including predicate subtypes. The PVS typechecker verifies simple type correctness and generates proof obligations for subtype membership, type equivalence, and termination. These proof obligations can be discharged interactively or automatically using pre-defined proof strategies. By carefully crafting the type constraints, PVS can be used as a general-purpose proof obligation generator. This has already been illustrated in an elegant structural embedding of the B method in PVS by Muñoz and Rushby. We demonstrate a similar structural embedding of a variant of Floyd’s method by defining a Floyd graph with a set of well-formedness conditions. When the graph is instantiated by an actual program annotated with assertions, the appropriate proof obligations are generated. The validity of these proof obligations implies the correctness of the program. The technique of defining templates for deriving proof obligations can be adapted to a number of other settings without the need for a specialized proof obligation generator or bespoke automation.