This is a small seep for Computer Science: a step towards a systematic proof-theory for programming-language semantics. We study a language that is designed to formalise assertions about how programs behave. In this language each program determines a modal connective that has the meaning ''after the program terminates ..,''. Such connectives appear in the ''algorithmic logic'' of A. Salwicki at Warsaw, but the explicit use of techniques from modal logic in this area was initiated more recently by V.R. Pratt at M.I.Т., and has become known as ''dynamic logic''. It is to the latter that the present work is directly related.