Semantics (computer science)

Last updated

In programming language theory, semantics is the rigorous mathematical study of the meaning of programming languages. [1] Semantics assigns computational meaning to valid strings in a programming language syntax. It is closely related to, and often crosses over with, the semantics of mathematical proofs.

Contents

Semantics describes the processes a computer follows when executing a program in that specific language. This can be done by describing the relationship between the input and output of a program, or giving an explanation of how the program will be executed on a certain platform, thereby creating a model of computation.

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 proofs of correctness, equivalence, and termination". [2] [3] Floyd further wrote: [2]

A semantic definition of a programming language, in our approach, is founded on a syntactic definition. It must specify which of the phrases in a syntactically correct program represent commands, and what conditions must be imposed on an interpretation in the neighborhood of each command.

In 1969, Tony Hoare published a paper on Hoare logic seeded by Floyd's ideas, now sometimes collectively called axiomatic semantics . [4] [5]

In the 1970s, the terms operational semantics and denotational semantics emerged. [5]

Overview

The field of formal semantics encompasses all of the following:

It has close links with other areas of computer science such as programming language design, type theory, compilers and interpreters, program verification and model checking.

Approaches

There are many approaches to formal semantics; these belong to three major classes:

Apart from the choice between denotational, operational, or axiomatic approaches, most variations in formal semantic systems arise from the choice of supporting mathematical formalism.[ citation needed ]

Variations

Some variations of formal semantics include the following:

Describing relationships

For a variety of reasons, one might wish to describe the relationships between different formal semantics. For example:

It is also possible to relate multiple semantics through abstractions via the theory of abstract interpretation.[ citation needed ]

See also

Related Research Articles

<span class="mw-page-title-main">Formal language</span> Sequence of words formed by specific rules

In logic, mathematics, computer science, and linguistics, a formal language consists of words whose letters are taken from an alphabet and are well-formed according to a specific set of rules called a formal grammar.

In computer science, denotational semantics is an approach of formalizing the meanings of programming languages by constructing mathematical objects that describe the meanings of expressions from the languages. Other approaches providing formal semantics of programming languages include axiomatic semantics and operational semantics.

In computer science, formal methods are mathematically rigorous techniques for the specification, development, analysis, and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analysis can contribute to the reliability and robustness of a design.

In linguistics and philosophy, the denotation of an expression is its literal meaning. For instance, the English word "warm" denotes the property of having high temperature. Denotation is contrasted with other aspects of meaning including connotation. For instance, the word "warm" may evoke calmness or coziness, but these associations are not part of the word's denotation. Similarly, an expression's denotation is separate from pragmatic inferences it may trigger. For instance, describing something as "warm" often implicates that it is not hot, but this is once again not part of the word's denotation.

In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of a system with respect to a certain formal specification or property, using formal methods of mathematics. Formal verification is a key incentive for formal specification of systems, and is at the core of formal methods. It represents an important dimension of analysis and verification in electronic design automation and is one approach to software verification. The use of formal verification enables the highest Evaluation Assurance Level (EAL7) in the framework of common criteria for computer security certification.

Operational semantics is a category of formal programming language semantics in which certain desired properties of a program, such as correctness, safety or security, are verified by constructing proofs from logical statements about its execution and procedures, rather than by attaching mathematical meanings to its terms. Operational semantics are classified in two categories: structural operational semantics formally describe how the individual steps of a computation take place in a computer-based system; by opposition natural semantics describe how the overall results of the executions are obtained. Other approaches to providing a formal semantics of programming languages include axiomatic semantics and denotational semantics.

A formal system is an abstract structure and formalization of an axiomatic system used for inferring theorems from axioms by a set of inference rules.

Computational semiotics is an interdisciplinary field that applies, conducts, and draws on research in logic, mathematics, the theory and practice of computation, formal and natural language studies, the cognitive sciences generally, and semiotics proper. The term encompasses both the application of semiotics to computer hardware and software design and, conversely, the use of computation for performing semiotic analysis. The former focuses on what semiotics can bring to computation; the latter on what computation can bring to semiotics.

Axiomatic semantics is an approach based on mathematical logic for proving the correctness of computer programs. It is closely related to Hoare logic.

<span class="mw-page-title-main">Concurrency (computer science)</span> Ability to execute a task in a non-serial manner

In computer science, concurrency is the ability of different parts or units of a program, algorithm, or problem to be executed out-of-order or in partial order, without affecting the outcome. This allows for parallel execution of the concurrent units, which can significantly improve overall speed of the execution in multi-processor and multi-core systems. In more technical terms, concurrency refers to the decomposability of a program, algorithm, or problem into order-independent or partially-ordered components or units of computation.

In semantics, mathematical logic and related disciplines, the principle of compositionality is the principle that the meaning of a complex expression is determined by the meanings of its constituent expressions and the rules used to combine them. The principle is also called Frege's principle, because Gottlob Frege is widely credited for the first modern formulation of it. However, the principle has never been explicitly stated by Frege, and arguably it was already assumed by George Boole decades before Frege's work.

In logic and mathematics, a formal proof or derivation is a finite sequence of sentences, each of which is an axiom, an assumption, or follows from the preceding sentences in the sequence by a rule of inference. It differs from a natural language argument in that it is rigorous, unambiguous and mechanically verifiable. If the set of assumptions is empty, then the last sentence in a formal proof is called a theorem of the formal system. The notion of theorem is not in general effective, therefore there may be no method by which we can always find a proof of a given sentence or determine that none exists. The concepts of Fitch-style proof, sequent calculus and natural deduction are generalizations of the concept of proof.

Predicate transformer semantics were introduced by Edsger Dijkstra in his seminal paper "Guarded commands, nondeterminacy and formal derivation of programs". They define the semantics of an imperative programming paradigm by assigning to each statement in this language a corresponding predicate transformer: a total function between two predicates on the state space of the statement. In this sense, predicate transformer semantics are a kind of denotational semantics. Actually, in guarded commands, Dijkstra uses only one kind of predicate transformer: the well-known weakest preconditions.

<span class="mw-page-title-main">Joseph Goguen</span> American computer scientist

Joseph Amadee Goguen was an American computer scientist. He was professor of Computer Science at the University of California and University of Oxford, and held research positions at IBM and SRI International.

<span class="mw-page-title-main">Gordon Plotkin</span> Computer Scientist

Gordon David Plotkin, is a theoretical computer scientist in the School of Informatics at the University of Edinburgh. Plotkin is probably best known for his introduction of structural operational semantics (SOS) and his work on denotational semantics. In particular, his notes on A Structural Approach to Operational Semantics were very influential. He has contributed to many other areas of computer science.

<span class="mw-page-title-main">Programming language theory</span> Branch of computer science

Programming language theory (PLT) is a branch of computer science that deals with the design, implementation, analysis, characterization, and classification of formal languages known as programming languages. Programming language theory is closely related to other fields including mathematics, software engineering, and linguistics. There are a number of academic conferences and journals in the area.

The term "information algebra" refers to mathematical techniques of information processing. Classical information theory goes back to Claude Shannon. It is a theory of information transmission, looking at communication and storage. However, it has not been considered so far that information comes from different sources and that it is therefore usually combined. It has furthermore been neglected in classical information theory that one wants to extract those parts out of a piece of information that are relevant to specific questions.

In computer science, algebraic semantics is a form of axiomatic semantics based on algebraic laws for describing and reasoning about program specifications in a formal manner.

<span class="mw-page-title-main">Formalism (linguistics)</span> Concept in linguistics

In linguistics, the term formalism is used in a variety of meanings which relate to formal linguistics in different ways. In common usage, it is merely synonymous with a grammatical model or a syntactic model: a method for analyzing sentence structures. Such formalisms include different methodologies of generative grammar which are especially designed to produce grammatically correct strings of words; or the likes of Functional Discourse Grammar which builds on predicate logic.

References

  1. Goguen, Joseph A. (1975). "Semantics of computation". Category Theory Applied to Computation and Control. Lecture Notes in Computer Science. Vol. 25. Springer. pp. 151–163. doi:10.1007/3-540-07142-3_75. ISBN   978-3-540-07142-6.
  2. 1 2 Floyd, Robert W. (1967). "Assigning Meanings to Programs" (PDF). In Schwartz, J.T. (ed.). Mathematical Aspects of Computer Science. Proceedings of Symposium on Applied Mathematics. Vol. 19. American Mathematical Society. pp. 19–32. ISBN   0821867288.
  3. Knuth, Donald E. "Memorial Resolution: Robert W. Floyd (1936–2001)" (PDF). Stanford University Faculty Memorials. Stanford Historical Society.
  4. Hoare, C. A. R. (October 1969). "An axiomatic basis for computer programming". Communications of the ACM . 12 (10): 576–580. doi: 10.1145/363235.363259 . S2CID   207726175.
  5. 1 2 Winskel, Glynn (1993). The formal semantics of programming languages : an introduction. Cambridge, Mass.: MIT Press. p.  xv. ISBN   978-0-262-23169-5.
  6. Schmidt, David A. (1986). Denotational Semantics: A Methodology for Language Development. William C. Brown Publishers. ISBN   9780205104505.
  7. Plotkin, Gordon D. (1981). A structural approach to operational semantics (Report). Technical Report DAIMI FN-19. Computer Science Department, Aarhus University.
  8. 1 2 Goguen, Joseph A.; Thatcher, James W.; Wagner, Eric G.; Wright, Jesse B. (1977). "Initial algebra semantics and continuous algebras". Journal of the ACM . 24 (1): 68–95. doi: 10.1145/321992.321997 . S2CID   11060837.
  9. Mosses, Peter D. (1996). Theory and practice of action semantics (Report). BRICS Report RS9653. Aarhus University.
  10. Deransart, Pierre; Jourdan, Martin; Lorho, Bernard (1988). "Attribute Grammars: Definitions, Systems and Bibliography. Lecture Notes in Computer Science 323. Springer-Verlag. ISBN   9780387500560.
  11. Lawvere, F. William (1963). "Functorial semantics of algebraic theories". Proceedings of the National Academy of Sciences of the United States of America . 50 (5): 869–872. Bibcode:1963PNAS...50..869L. doi: 10.1073/pnas.50.5.869 . PMC   221940 . PMID   16591125.
  12. Andrzej Tarlecki; Rod M. Burstall; Joseph A. Goguen (1991). "Some fundamental algebraic tools for the semantics of computation: Part 3. Indexed categories". Theoretical Computer Science . 91 (2): 239–264. doi: 10.1016/0304-3975(91)90085-G .
  13. Batty, Mark; Memarian, Kayvan; Nienhuis, Kyndylan; Pichon-Pharabod, Jean; Sewell, Peter (2015). "The problem of programming language concurrency semantics" (PDF). Proceedings of the European Symposium on Programming Languages and Systems. Springer. pp. 283–307. doi: 10.1007/978-3-662-46669-8_12 .
  14. Abramsky, Samson (2009). "Semantics of interaction: An introduction to game semantics". In Andrew M. Pitts; P. Dybjer (eds.). Semantics and Logics of Computation. Cambridge University Press. pp. 1–32. doi:10.1017/CBO9780511526619.002. ISBN   9780521580571.
  15. Dijkstra, Edsger W. (1975). "Guarded commands, nondeterminacy and formal derivation of programs". Communications of the ACM . 18 (8): 453–457. doi: 10.1145/360933.360975 . S2CID   1679242.

Further reading

Textbooks
Lecture notes