Added Hoare triples for all of the semantic commands, strutural rules,
the read command, and method calls.