The material in these lecture notes offers an exposition - aijned at graduate students rather than researchers in the field - of a topic often called ''program schemata'' or ''schematology''. The subject matter represents one approach to formalizing the elusive notion of the ''semantics of programming languages''. The idea is to model an ''abstract flowchart'' and study the interrelation between the syntax of programs (what can be said about their behavior from their format) and the semantics (what they actually ''do'', depending on the interpretation, the programming language, and perhaps even the implementation) and examine the application of formal proof systems to verify properties of programs.