Editing Semantics (computer science) (section)

==History==

In 1967, [[Robert W. Floyd]] published the paper ''Assigning meanings to programs''; his chief aim was "a rigorous standard for proofs about computer programs, including [[formal verification|proofs of correctness]], equivalence, and termination".<ref name=floyd>{{cite book |year=1967 |author-link=Robert W. Floyd |first=Robert W. |last=Floyd |chapter=Assigning Meanings to Programs |chapter-url=https://people.eecs.berkeley.edu/~necula/Papers/FloydMeaning.pdf |editor-first=J.T. |editor-last=Schwartz |title=Mathematical Aspects of Computer Science |publisher=American Mathematical Society |isbn=0821867288 |pages=19–32 |url=https://books.google.com/books?id=ynigSICJflYC |series=Proceedings of Symposium on Applied Mathematics |volume=19 }}</ref><ref>{{cite web |author-link=Donald Knuth|author-first=Donald E.|author-last=Knuth |title=Memorial Resolution: Robert W. Floyd (1936–2001) |url=https://stacks.stanford.edu/file/druid:zy788sr3998/SC0193_MemorialResolution_Floyd_Robert.pdf |work=Stanford University Faculty Memorials |publisher=Stanford Historical Society }}</ref> Floyd further wrote:{{r|floyd}}
<blockquote>
A semantic definition of a programming language, in our approach, is founded on a [[Syntax (programming languages)|syntactic]] definition. It must specify which of the phrases in a syntactically correct program represent [[Command (computing)|commands]], and what [[Conditional (computer programming)|conditions]] must be imposed on an interpretation in the neighborhood of each command.
</blockquote>

In 1969, [[Tony Hoare]] published a paper on [[Hoare logic]] seeded by Floyd's ideas, now sometimes collectively called ''[[axiomatic semantics]]''.<ref name="hoare">{{Cite journal
 |last=Hoare 
 |first=C. A. R. 
 |authorlink=Tony Hoare 
 |title=An axiomatic basis for computer programming 
 |doi=10.1145/363235.363259 
 |journal=[[Communications of the ACM]] 
 |volume=12 
 |issue=10 
 |pages=576–580 
 |date=October 1969 
 |s2cid=207726175 
 |doi-access=free 
 }}</ref>{{r|winskel}}

In the 1970s, the terms ''[[operational semantics]]'' and ''[[denotational semantics]]'' emerged.<ref name=winskel>{{cite book |last1=Winskel |first1=Glynn |title=The formal semantics of programming languages : an introduction |date=1993 |publisher=MIT Press |location=Cambridge, Mass. |isbn=978-0-262-23169-5 |page=[https://archive.org/details/formalsemanticso0000wins/page/n17 xv] |url=https://archive.org/details/formalsemanticso0000wins}}</ref>