In A Deterministic program there is at most one instruction to be executed “next,” so that from a given initial state only one execution sequence is generated. In classical programming languages like Pascal, only deterministic programs can be written. In this chapter we study a small class of deterministic programs, called while programs, which are included in all other classes of programs studied in this book. We start by defining the syntax (Section 3.1), then introduce an operational semantics (Section 3.2), subsequently study program verification by introducing proof systems allowing us to prove various program properties and prove the soundness of the introduced proof systems (Section 3.3). This pattern is repeated for all classes of programs studied in this book. We introduce here two semantics —partial correctness and total correctness semantics. The former does not take into account the possibility of divergence while the latter does.
Weitere Kapitel dieses Buchs durch Wischen aufrufen
Bitte loggen Sie sich ein, um Zugang zu diesem Inhalt zu erhalten
Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:
- While Programs
- Springer London
- Chapter 3
ec4u, Neuer Inhalt/© ITandMEDIA