UMBC CMSC 331 notes (9/16/2004)CMSC 331, Some material © 1998 by Addison Wesley Longman, Inc. 1CMSC 331, Some material © 1998 by Addison Wesley Longman, Inc. 2• 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 Sebesta 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 semanticsCMSC 331, Some material © 1998 by Addison Wesley Longman, Inc. 3• 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_verificationCMSC 331, Some material © 1998 by Addison Wesley Longman, Inc. 4• 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?UMBC CMSC 331 notes (9/16/2004)CMSC 331, Some material © 1998 by Addison Wesley Longman, Inc. 5• 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, unrepairable applications (e.g., Martian rover)• Hardware design (e.g. Pentium chip)CMSC 331, Some material © 1998 by Addison Wesley Longman, Inc. 6• It took the European Space Agency 10 years and $7 billion to produceAriane 5, a giant rocket capable ofhurling a pair of three-ton satellitesinto orbit with each launch andintended to give Europeoverwhelming supremacy in thecommercial space business.• All it took to explode the rocket lessthan a minute into its maiden voyagein June 1996, scattering fiery rubble across the mangrove swamps of French Guiana, was a small computer program trying to stuff a 64-bit number into a 16-bit space.CMSC 331, Some material © 1998 by Addison Wesley Longman, Inc. 7• In the mid 90’s a bug was found inthe floating point hardware in Intel’slatest Pentium microprocessor.• Unfortunately, the bug was only foundafter many had been made and sold.• The bug was subtle, effecting only the 9thdecimal place of some computations.• But users cared.• Intel had to recall the chips and took a $500M write-offCMSC 331, Some material © 1998 by Addison Wesley Longman, Inc. 8• 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 correctnessUMBC CMSC 331 notes (9/16/2004)CMSC 331, Some material © 1998 by Addison Wesley Longman, Inc. 9• Next we’ll look at issues close to the syntax end, what Sebesta 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 semanticsCMSC 331, Some material © 1998 by Addison Wesley Longman, Inc. 10Static semantics covers some language features that are 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 it’s input. Categories attribute grammars can handle:• Context-free but cumbersome (e.g. type checking)• Noncontext-free (e.g. variables must be declared before they are used)CMSC 331, Some material © 1998 by Addison Wesley Longman, Inc. 11• Attribute Grammars (AGs) were developed by Donald Knuth ~1968• Motivation:• CFGs cannot describe all of the syntax of programming languages• Additions to CFGs to annotate the parse tree with some “semantic” info• Primary value of AGs:• Static semantics specification• Compiler design (static semantics checking)CMSC 331, Some material © 1998 by Addison Wesley Longman, Inc. 12Attribute Grammar Example•Ada has this rule to describe procedure definitions:<proc> => procedure <procName> <procBody> end <procName> ;•But the name after “procedure” has to be the same as the name after “end”.•This is not possible to capture in a CFG (in practice) because there are too many names.•Solution: annotate parse tree nodes with attributes and add a “semantic” rules or constraints to the syntactic rule in the grammar.<proc> => procedure <procName>[1] <procBody> end <procName>[2] ;<procName][1].string = <procName>[2].stringUMBC CMSC 331 notes (9/16/2004)CMSC 331, Some material © 1998 by Addison Wesley Longman, Inc. 13Attribute GrammarsDef: An attribute grammar is a CFG G=(S,N,T,P)with the following additions:–For each grammar symbol x there is a set A(x) of attribute values.–Each rule has a set of functions that define certain attributes of the nonterminals in the rule.–Each rule has a (possibly empty) set of predicates to check for attribute consistencyCMSC 331, Some material © 1998 by Addison Wesley Longman, Inc. 14Attribute GrammarsDef: An attribute grammar is a CFG G=(S,N,T,P)with the following additions:– For each grammar symbol x there is a set A(x) of attribute values.– Each rule has a set