No label defined (Q3976060)

[For the entire collection see Zbl 0731.00025.] Structural Operational Semantics (SOS) is a powerful approach to the formal description of programming languages. As an improvement on SOS, Inductive Semantics has been introduced by \textit{E. Astesiano} in the book ``Formal Description of Programming Concepts'' by \textit{E. J. Neuhold} and \textit{M. Paul} (eds.) [Berlin etc., (1990; Zbl 0743.68010)]. `Inductive' means that the various semantic definitions are all inductive definitions of families of sets associated with inductive system. The author presents an inductive nonstandard semantics. To apply this semantics, the author introduces a small Pascal-like language-WHILE and defines the histories for WHILE formally. An inductive system STAT is given for the static semantics of WHILE, it is shown that a program \(P\) is statically correct iff \(P\vdash OK\) can be proved in STAT. And an inductive system \(SEM\) is given for the dynamic semantic of WHILE, it is shown that a program \(P\) returns a result \(r\) starting from an input \(i\) iff \(P\vdash i,r\) can be proved in \(SEM\). From the system \(SEM\), the author derives naturally a denotational semantics for the language. The semantics of this paper has the advantages of being more abstract and of avoiding the explicit use of environments and store.