1 CMSC 331, Some material © 1998 by Addison Wesley Longman, Inc. Semantics Overview •  Syntax is about “form” and semantics about “meaning”. –  The boundary between syntax and semantics is not always clear. •  First we’ll motivate why semantics matters. •  Then we’ll look at issues close to the syntax end, what some calls “static semantics”, and the technique of attribute grammars. •  Then we’ll sketch three approaches to defining “deeper” semantics (1) Operational semantics (2) Axiomatic semantics (3) Denotational semantics 2 CMSC 331, Some material © 1998 by Addison Wesley Longman, Inc. Motivation •  Capturing what a program in some programming language means is very difficult •  We can’t really do it in any practical sense – For most work-a-day programming languages (e.g., C, C++, Java, Perl, C#). – For large programs •  So, why is worth trying? •  One reason: program verification! Program Verification: the process of formal proving, that the computer program does exactly what is stated in the program specification it was written to realize. http://www.wikipedia.org/wiki/Program_verification 3 CMSC 331, Some material © 1998 by Addison Wesley Longman, Inc. Program Verification •  Program verification can be done for simple programming languages and small or moderately sized programs •  It requires a formal specification for what the program should do – e.g., what it’s inputs will be and what actions it will take or output it will generate given the inputs •  That’s a hard task in itself! •  There are applications where it is worth it to (1) use a simplified programming language, (2) work out formal specs for a program, (3) capture the semantics of the simplified PL and (4) do the hard work of putting it all together and proving program correctness. •  What are they? 4 CMSC 331, Some material © 1998 by Addison Wesley Longman, Inc. Program Verification •  There are applications where it is worth it to (1) use a simplified programming language, (2) work out formal specs for a program, (3) capture the semantics of the simplified PL and (4) do the hard work of putting it all together and proving program correctness. Like… •  Security and encryption •  Financial transactions •  Applications on which lives depend (e.g., healthcare, aviation) •  Expensive, one-shot, un-repairable applications (e.g., Martian rover) •  Hardware design (e.g. Pentium chip) 5 CMSC 331, Some material © 1998 by Addison Wesley Longman, Inc. Double Int kills Ariane 5 • It took the European Space Agency 10 years and $7B to produce Ariane 5, a giant rocket capable of hurling a pair of three-ton satellites into orbit with each launch and intended to give Europe supremacy in the commercial space business • All it took to explode the rocket less than a minute into its maiden voyage in 1996 was a small computer program trying to stuff a 64-bit number into a 16-bit space. 6 CMSC 331, Some material © 1998 by Addison Wesley Longman, Inc. Intel Pentium Bug •  In the mid 90’s a bug was found in the floating point hardware in Intel’s latest Pentium microprocessor •  Unfortunately, the bug was only found after many had been made and sold •  The bug was subtle, effecting only the 9th decimal place of some computations •  But users cared •  Intel had to recall the chips, taking a $500M write-off 7 CMSC 331, Some material © 1998 by Addison Wesley Longman, Inc. So… •  While automatic program verification is a long range goal … •  Which might be restricted to applications where the extra cost is justified •  We should try to design programming languages that help, rather than hinder, our ability to make progress in this area. •  We should continue research on the semantics of programming languages … •  And the ability to prove program correctness 8 CMSC 331, Some material © 1998 by Addison Wesley Longman, Inc. Semantics •  Next we’ll look at issues close to the syntax end, what some calls “static semantics”, and the technique of attribute grammars. •  Then we’ll sketch three approaches to defining “deeper” semantics (1) Operational semantics (2) Axiomatic semantics (3) Denotational semantics 9 CMSC 331, Some material © 1998 by Addison Wesley Longman, Inc. Static Semantics • Static semantics covers some language features difficult or impossible to handle in a BNF/CFG • It is also a mechanism for building a parser which produces a “abstract syntax tree” of its input • Attribute grammars are one common technique • Categories attribute grammars can handle: •  Context-free but cumbersome (e.g. type checking) •  Non-context-free (e.g. variables must be declared before they are used) 10 CMSC 331, Some material © 1998 by Addison Wesley Longman, Inc.