This paper presents a special subset of the first-order predicate logic named
S-program calculus (briefly S-calculus). The S-calculus is a calculus
consisting of so-called S-formulas that are defined over the abstract state
space of a virtual machine. We show that S-formulas are a highly general tool
for analyzing program semantics inasmuch as Hoare triplets of total and partial
correctness are not more than two S-formulas. Moreover, all the rules of Hoare
logic can be derived using S-formulas and axioms/theorems of first-order
predicate calculus.