0% found this document useful (0 votes)
1 views19 pages

Chapter3 Syntax Semantics Notes

Uploaded by

ayeshaahh26
Copyright
© All Rights Reserved
We take content rights seriously. If you suspect this is your content, claim it here.
Available Formats
Download as DOCX, PDF, TXT or read online on Scribd
0% found this document useful (0 votes)
1 views19 pages

Chapter3 Syntax Semantics Notes

Uploaded by

ayeshaahh26
Copyright
© All Rights Reserved
We take content rights seriously. If you suspect this is your content, claim it here.
Available Formats
Download as DOCX, PDF, TXT or read online on Scribd

CHAPTER 3

Describing Syntax and Semantics


Concepts of Programming Languages — Robert W. Sebesta (11th Edition)
Supplemented with: Introduction to Programming Languages — Anthony A. Aaby

Topics Covered
• 3.1 Introduction — Syntax vs Semantics
• 3.2 The General Problem of Describing Syntax (Lexemes, Tokens, Recognizers,
Generators)
• 3.3 Formal Methods: BNF, CFG, EBNF — with Derivations, Parse Trees, Ambiguity,
Precedence, Associativity
• 3.4 Attribute Grammars — Static Semantics, Synthesized & Inherited Attributes
• 3.5 Dynamic Semantics: Operational, Denotational, Axiomatic Semantics
• Pragmatics (from Aaby)

3.1 Introduction
Programming language description must be precise enough for three audiences: initial evaluators,
implementors (compiler writers), and language users. Imprecise definitions lead to dialects; overly
complex ones reduce adoption (as happened with ALGOL 60 and ALGOL 68).

Term Definition
Syntax The FORM of a language's expressions, statements, and program units.
Describes how things look/are structured.
Semantics The MEANING of those expressions, statements, and program units.
Describes what they do.
Relationship In a well-designed language, semantics should follow directly from syntax —
the appearance should suggest the meaning.

Example: Java while statement


Syntax: while (boolean_expr) statement

Semantics: When boolean_expr is true, execute the embedded statement,


then return to re-evaluate the boolean_expr.
When boolean_expr is false, transfer control past the loop.

3.2 The General Problem of Describing Syntax


A language is a set of strings of characters from some alphabet. The syntax rules specify which
strings belong to the language.

3.2.1 Key Terminology


Term Definition
Sentence / A string belonging to the language.
Statement
Lexeme The smallest syntactic unit (e.g., numeric literals, operators, keywords,
identifiers). Programs are strings of lexemes.
Token A category/group of lexemes. For example, 'identifier' is a token that covers
sum, total, count, etc.

Example: Java statement: index = 2 * count + 17;


Lexeme Token
------ -----
index -> identifier
= -> equal_sign
2 -> int_literal
* -> mult_op
count -> identifier
+ -> plus_op
17 -> int_literal
; -> semicolon

3.2.2 Language Recognizers


• A recognizer is a device R that reads strings and accepts or rejects them depending on
whether they belong to language L.
• The syntax analyzer (parser) of a compiler is a recognizer — it checks whether programs
are syntactically correct.
• Parsers are discussed in depth in Chapter 4 (Sebesta).

3.2.3 Language Generators


• A generator produces sentences of the language when "triggered".
• Generators are more human-readable than recognizers — you can compare a statement
against the generator's structure to check syntax.
• BNF/CFG are generator-based formal methods.
• Close relationship: given a CFG (generator), a recognizer can be algorithmically
constructed.

3.3 Formal Methods of Describing Syntax


3.3.1 Context-Free Grammars (CFG) and BNF
Origins
• Noam Chomsky (mid-1950s): described four classes of grammars. Context-free and
regular grammars turned out useful for programming languages.
• John Backus (1959): introduced a new formal notation for ALGOL 58, later modified by
Peter Naur for ALGOL 60 — became BNF (Backus-Naur Form).
• BNF and CFG are essentially identical. The terms are used interchangeably.

What is a Context-Free Grammar?


A CFG consists of:
• A set of terminal symbols (actual tokens/lexemes of the language)
• A set of non-terminal symbols (abstractions, written in <angle brackets>)
• A set of production rules (each maps a nonterminal to a sequence of terminals and/or
nonterminals)
• A start symbol (top-level nonterminal, often <program>)

BNF Fundamentals
• BNF is a metalanguage — a language used to describe another language.
• Each rule has a Left-Hand Side (LHS) and a Right-Hand Side (RHS) separated by →
• LHS: a single nonterminal
• RHS: a mix of terminals and nonterminals
• Multiple definitions are separated by | (logical OR)

Example BNF rules:

<assign> -> <var> = <expression>


<if_stmt> -> if ( <logic_expr> ) <stmt>
| if ( <logic_expr> ) <stmt> else <stmt>
<ident_list> -> identifier
| identifier , <ident_list> (recursion for lists)
Describing Lists Using Recursion
BNF has no ellipsis (...), so lists are defined using recursive rules:
<ident_list> -> identifier
| identifier , <ident_list>

This defines a list as: a single identifier OR


an identifier followed by a comma and another <ident_list>.

3.3.2 Derivations
A derivation is the sequence of rule applications starting from the start symbol, replacing
nonterminals step by step until only terminals remain.
• Each string in the derivation is called a sentential form.
• The symbol => means 'derives'.
• Leftmost derivation: always replace the leftmost nonterminal first.
• Rightmost derivation: always replace the rightmost nonterminal first.
• Derivation order does not affect the language generated.

Example 3.1: Grammar for a Small Language


<program> -> begin <stmt_list> end
<stmt_list> -> <stmt> | <stmt> ; <stmt_list>
<stmt> -> <var> = <expression>
<var> -> A | B | C
<expression> -> <var> + <var> | <var> - <var> | <var>

Leftmost derivation of: begin A = B + C ; B = C end


<program>
=> begin <stmt_list> end
=> begin <stmt> ; <stmt_list> end
=> begin <var> = <expression> ; <stmt_list> end
=> begin A = <expression> ; <stmt_list> end
=> begin A = <var> + <var> ; <stmt_list> end
=> begin A = B + <var> ; <stmt_list> end
=> begin A = B + C ; <stmt_list> end
=> begin A = B + C ; <stmt> end
=> begin A = B + C ; <var> = <expression> end
=> begin A = B + C ; B = <expression> end
=> begin A = B + C ; B = <var> end
=> begin A = B + C ; B = C end

3.3.3 Parse Trees


A parse tree is a hierarchical tree structure representing the syntactic structure of a sentence
derived by a grammar.
• Every internal node is labeled with a nonterminal symbol.
• Every leaf node is labeled with a terminal symbol.
• Every subtree describes one instance of an abstraction.
• Parse trees are one of the most attractive features of grammars.

Example 3.2: Grammar for Simple Assignment Statements


<assign> -> <id> = <expr>
<id> -> A | B | C
<expr> -> <id> + <expr> | <id> * <expr> | ( <expr> ) | <id>

Leftmost derivation of A = B * (A + C):


<assign>
=> <id> = <expr>
=> A = <expr>
=> A = <id> * <expr>
=> A = B * <expr>
=> A = B * ( <expr> )
=> A = B * ( <id> + <expr> )
=> A = B * ( A + <expr> )
=> A = B * ( A + <id> )
=> A = B * ( A + C )

The parse tree for A = B * (A + C) looks like:


<assign>
/ | \
<id> = <expr>
| / | \
A <id> * <expr>
| / | \
B ( <expr> )
/ | \
<id> + <expr>
| |
A <id>
|
C

3.3.4 Ambiguity
A grammar is ambiguous if a sentential form has TWO or more distinct parse trees.
• Ambiguity is a problem because compilers choose what code to generate based on the
parse tree structure.
• If two parse trees exist for the same sentence, the meaning cannot be determined uniquely.

Example 3.3: Ambiguous Grammar


<assign> -> <id> = <expr>
<id> -> A | B | C
<expr> -> <expr> + <expr> | <expr> * <expr> | ( <expr> ) | <id>

The sentence A = B + C * A has TWO distinct parse trees:


Tree 1: * is lower (evaluated first) -> correct math precedence
Tree 2: + is lower (evaluated first) -> wrong math precedence
=> Grammar is AMBIGUOUS.

3.3.5 Operator Precedence


Precedence determines which operator is evaluated first when two different operators appear in an
expression (e.g., x + y * z).
• Higher precedence = evaluated first.
• In a parse tree: operators lower in the tree are evaluated FIRST.
• To specify precedence, use separate nonterminals for operands of operators with different
precedence levels.

Example 3.4: Unambiguous Grammar with Correct Precedence


<assign> -> <id> = <expr>
<id> -> A | B | C
<expr> -> <expr> + <term> | <term> (* addition at top, lower precedence *)
<term> -> <term> * <factor> | <factor> (* multiplication lower, higher precedence *)
<factor> -> ( <expr> ) | <id>

In this grammar: * always appears LOWER in the parse tree than +


=> * is always evaluated before + (correct math precedence)

3.3.6 Associativity of Operators


When an expression has two operators of the same precedence (e.g., A / B * C), associativity
determines which is evaluated first.
• Left associativity: A / B * C = (A / B) * C — most common
• Right associativity: A ** B ** C = A ** (B ** C) — typical for exponentiation
• Left recursive rule: LHS appears at the beginning of RHS — specifies left associativity
◦ Example: <expr> -> <expr> + <term> (left recursive)
• Right recursive rule: LHS appears at the end of RHS — specifies right associativity
◦ Example: <factor> -> <exp> ** <factor> (right recursive)

For right-associative exponentiation:


<factor> -> <exp> ** <factor> | <exp>
<exp> -> ( <expr> ) | id

3.3.7 Dangling else / Ambiguous if-else


The BNF rules for if-else can create ambiguity (the 'dangling else' problem):
Ambiguous:
if (done == true)
if (denom == 0) quotient = 0;
else quotient = num / denom; <-- which 'if' does this else belong to?

Solution: Distinguish matched from unmatched statements:


<stmt> -> <matched> | <unmatched>
<matched> -> if (<logic_expr>) <matched> else <matched>
| any non-if statement
<unmatched> -> if (<logic_expr>) <stmt>
| if (<logic_expr>) <matched> else <unmatched>

Rule: an else clause always matches the nearest previous unmatched 'then'.

3.3.8 Extended BNF (EBNF)


EBNF adds notational conveniences to BNF without increasing its expressive power. Three main
extensions:

Symbol Meaning Example


[ ] Optional part (0 or 1 <if_stmt> -> if (<expr>) <stmt> [else <stmt>]
times)
{ } Repeat 0 or more <ident_list> -> <identifier> {, <identifier>}
times (replaces
recursion)
( | ) Choose one from <term> -> <term> (* | / | %) <factor>
multiple options

BNF vs EBNF Comparison (Example 3.5)


BNF Version: EBNF Version:
<expr> -> <expr> + <term> <expr> -> <term> {(+ | -) <term>}
| <expr> - <term> <term> -> <factor> {(* | /) <factor>}
| <term> <factor>-> <exp> {** <exp>}
<term> -> <term> * <factor> <exp> -> (<expr>) | id
| <term> / <factor>
| <factor>
<factor>-> <exp> ** <factor> | <exp>
<exp> -> (<expr>) | id

Note: EBNF is more compact. BNF naturally specifies left-associativity;


EBNF requires the parser to enforce associativity explicitly.

3.4 Attribute Grammars


3.4.1 Static Semantics — What it is and Why it Exists
Some language rules are too complex or outright impossible to express in BNF alone. These fall
under 'static semantics'.

Problem Example
Difficult (but possible) to express in Type compatibility rules (e.g., float cannot be assigned to int
BNF in Java). Possible in BNF but would make the grammar too
large.
Impossible to express in BNF Variables must be declared before use. Proven to be not
expressible in BNF.

• Static semantics rules concern the legal forms of programs (compile-time checks, not
runtime behavior).
• They are called 'static' because they can be checked at compile time.
• Attribute grammars, designed by Knuth (1968), handle both syntax and static semantics.

3.4.2 Attribute Grammar — Definition


An attribute grammar is a CFG extended with:
• Attributes: associated with each grammar symbol (terminal or nonterminal). Like variables
— they can hold values.
• Attribute computation functions (semantic functions): associated with grammar rules,
specifying how attribute values are computed.
• Predicate functions: Boolean expressions over attributes that enforce static semantic
rules. A false predicate indicates a violation.

3.4.3 Two Types of Attributes


Type Direction of Information Flow Computed From
Synthesized attribute Bottom-up: passes information UP Only from the node's children
the parse tree
Inherited attribute Top-down: passes information From the node's parent and/or
DOWN and ACROSS the tree siblings

Intrinsic Attributes
• These are synthesized attributes of leaf nodes whose values come from outside the parse
tree (e.g., from the symbol table).
• Example: the type of a variable comes from its earlier declaration stored in the symbol table.

3.4.4 Attribute Grammar Example: Ada Procedure Name Check


This example shows a rule that CANNOT be stated in BNF: the name after 'end' in an Ada
procedure must match the procedure's name.
Syntax rule: <proc_def> -> procedure <proc_name>[1]
<proc_body> end <proc_name>[2] ;

Predicate: <proc_name>[1].string == <proc_name>[2].string

=> If the names don't match, the predicate is FALSE -> error flagged.
Subscripts [1] and [2] distinguish the two occurrences of <proc_name>.

3.4.5 Attribute Grammar Example: Type Checking (Example 3.6)


This example shows how attribute grammars handle type checking for assignment statements.
Language rules: variables are A, B, or C; they can be int or real. In expressions with two variables,
if both are int, result is int; otherwise real. The assignment is valid only if left-side type equals right-
side type.

Syntax:
<assign> -> <var> = <expr>
<expr> -> <var>[2] + <var>[3] | <var>
<var> -> A | B | C

Attributes:
actual_type (synthesized) on <var> and <expr>: stores actual type (int or real)
expected_type (inherited) on <expr>: stores expected type from left-side
variable

Semantic rules:
1. <assign> -> <var> = <expr>
<expr>.expected_type <- <var>.actual_type

2. <expr> -> <var>[2] + <var>[3]


<expr>.actual_type <-
if (<var>[2].actual_type = int) AND (<var>[3].actual_type = int)
then int else real
Predicate: <expr>.actual_type == <expr>.expected_type

3. <expr> -> <var>


<expr>.actual_type <- <var>.actual_type
Predicate: <expr>.actual_type == <expr>.expected_type

4. <var> -> A | B | C
<var>.actual_type <- look-up(<var>.string) [looks up type in symbol table]

Computing Attribute Values (Decorating the Parse Tree)


For the sentence A = A + B (where A is real, B is int):
Step 1: <var>.actual_type <- look-up(A) = real (Rule 4)
Step 2: <expr>.expected_type <- <var>.actual_type = real (Rule 1)
Step 3: <var>[2].actual_type <- look-up(A) = real (Rule 4)
<var>[3].actual_type <- look-up(B) = int (Rule 4)
Step 4: <expr>.actual_type <- real (because one operand is real) (Rule 2)
Step 5: Predicate check: real == real => TRUE => Assignment is valid.

3.4.6 Evaluation of Attribute Grammars


• Every compiler implicitly uses attribute grammar concepts for static semantic checks.
• Attribute grammars are powerful but have high complexity and cost for real languages.
• Large number of attributes and semantic rules make them hard to write/read.
• Evaluating attribute values on large parse trees is computationally expensive.

3.5 Dynamic Semantics


Dynamic semantics describes the MEANING of programs — what happens when they execute.
Unlike syntax description, no single universally accepted notation exists for semantics.
Three main methods: Operational, Denotational, and Axiomatic Semantics.

3.5.1 Operational Semantics


The meaning of a statement or program is defined by specifying the effect of running it on a
machine. Meaning = sequence of state changes in machine storage.

• Basic idea: write a test program and observe its behavior — that is informal operational
semantics.
• Formal approach: use an intermediate-level language and an idealized virtual machine (not
a real computer, as real machines are too complex).

Two Levels of Operational Semantics


• Natural operational semantics: concerned with the final result of executing a complete
program.
• Structural operational semantics: concerned with the complete sequence of state
changes (step-by-step).

Basic Process
• Design an intermediate language with clear, unambiguous semantics.
• Construct a virtual machine (interpreter) to execute the intermediate language.
• Translate programming language constructs into the intermediate language.

Example: C for loop described in terms of simpler statements (operational semantics):


C Statement: Operational Meaning:
for (expr1; expr2; expr3) { expr1;
... loop: if expr2 == 0 goto out
} ...
expr3;
goto loop
out: ...

Intermediate language statements used to describe simple control structures:


ident = var
ident = ident + 1
ident = ident - 1
goto label
if var relop var goto label
ident = var bin_op var
ident = un_op var

where relop is one of: =, <>, >, <, >=, <=

Historical Use
• First major use: Vienna Definition Language (VDL) for PL/I (Wegner, 1972).
• VDL was so complex it was not practically useful.

Evaluation
• Good for language users and implementors when descriptions are kept simple and informal.
• Weakness: depends on programming languages, not mathematics — can lead to circularity.
• Less rigorous than axiomatic or denotational semantics.

3.5.2 Denotational Semantics


Denotational semantics is the most rigorous formal method for describing program meaning. Based
on recursive function theory (Scott and Strachey, 1971).
• For each language entity, define a mathematical object AND a mapping function.
• The mapping function maps syntactic constructs to their mathematical denotations
(meanings).
• Syntactic domain: the set of syntactic structures being mapped.
• Semantic domain: the set of mathematical objects that represent meaning.

Denotational vs Operational
Operational Semantics Denotational Semantics
Maps constructs to simpler language constructs Maps constructs to mathematical objects
(sets/functions)
State changes defined by coded algorithms State changes defined by mathematical functions
Models step-by-step execution Does NOT model step-by-step execution

Example: Binary Numbers (Denotational Mapping)


Grammar for binary numbers:
<bin_num> -> '0' | '1' | <bin_num> '0' | <bin_num> '1'

Semantic function Mbin maps binary number strings to decimal numbers (N = set of nonneg
integers):
Mbin('0') = 0
Mbin('1') = 1
Mbin(<bin_num> '0') = 2 * Mbin(<bin_num>)
Mbin(<bin_num> '1') = 2 * Mbin(<bin_num>) + 1

Example: 110 in binary


Mbin('110')
= Mbin('11' '0') -> 2 * Mbin('11')
= 2 * Mbin('1' '1') -> 2 * (2*Mbin('1') + 1)
= 2 * (2*1 + 1) = 2 * 3 = 6

The State of a Program


Program state s = a set of ordered pairs: s = {<i1,v1>, <i2,v2>, ..., <in,vn>}
• Each i is a variable name, each v is its current value.
• VARMAP(ij, s) = vj (the current value of variable ij in state s).
• Special value 'undef' indicates a variable is currently undefined.
• Most semantic mapping functions map states to states.

Denotational Semantics: Expressions


Me(<expr>, s) =
case <expr> of
<dec_num> => Mdec(<dec_num>, s)
<var> => if VARMAP(<var>, s) == undef
then error
else VARMAP(<var>, s)
<binary_expr> =>
if (Me(<binary_expr>.<left_expr>, s) == undef OR
Me(<binary_expr>.<right_expr>, s) == undef)
then error
else if (<binary_expr>.<operator> == '+')
then Me(left, s) + Me(right, s)
else Me(left, s) * Me(right, s)

Denotational Semantics: Assignment Statements


Ma(x = E, s) =
if Me(E, s) == error
then error
else s' = {<i1,v1'>, ..., <in,vn'>}, where for j=1..n:
if ij == x then vj' = Me(E, s)
else vj' = VARMAP(ij, s)

=> The assignment updates variable x to the evaluated value of E,


leaving all other variables unchanged.

Denotational Semantics: While Loop


Ml(while B do L, s) =
if Mb(B, s) == undef then error
else if Mb(B, s) == false then s
else if Msl(L, s) == error then error
else Ml(while B do L, Msl(L, s))

=> The loop is converted from iteration to recursion.


Recursion is mathematically easier to define with rigor.
Note: definition may compute nothing if loop doesn't terminate.

Evaluation
• Most rigorous method — provides concise, exact language descriptions.
• Used as aid in language design: if a construct's denotational description is complex, the
construct may be hard to use.
• Too complex for language users; useful for theoreticians and language designers.
• Has been used for automatic compiler generation research, but not yet practical for
industrial compilers.

3.5.3 Axiomatic Semantics


Axiomatic semantics is based on mathematical logic. Instead of directly specifying the meaning, it
specifies what can be PROVEN about a program. Developed specifically for proving program
correctness.
• Notation used: predicate calculus.
• Each statement is preceded and followed by logical expressions (assertions) that constrain
program variables.
• Precondition: assertion BEFORE a statement — constraints that must hold before
execution.
• Postcondition: assertion AFTER a statement — constraints that hold after execution.

Notation
{P} S {Q}
Where: P = precondition, S = statement, Q = postcondition

Example: {x > 3} x = x - 3 {x > 0}


This states: if x > 3 before the statement, then x > 0 after it.

Weakest Precondition
The weakest precondition is the LEAST RESTRICTIVE precondition that guarantees the
postcondition.
• Given a statement and postcondition, compute the weakest precondition.
• If the weakest preconditions can be computed for all statement types, they define the
language's semantics.

Assignment Axiom
For assignment statement x = E with postcondition Q:
Weakest precondition P = Q(x -> E)

Meaning: replace ALL occurrences of x in Q with E.

Examples:
a = b/2 - 1 {a < 10}
P: substitute a with b/2-1 in {a < 10}:
b/2 - 1 < 10 => b < 22
Weakest precondition: {b < 22}

x = 2*y - 3 {x > 25}


P: substitute x with 2*y-3 in {x > 25}:
2*y - 3 > 25 => y > 14
Weakest precondition: {y > 14}

x = x + y - 3 {x > 10}
P: substitute x with x+y-3 in {x > 10}:
x + y - 3 > 10 => y > 13 - x
Weakest precondition: {y > 13 - x}
Rule of Consequence
If {P} S {Q} is true, then:
{P} S {Q}, P' => P, Q => Q'
------------------------
{P'} S {Q'}

Meaning: a postcondition can be weakened, and a precondition can be strengthened.

Example: {x > 3} x = x-3 {x > 0} is proven.


Since {x > 5} => {x > 3}, by the rule of consequence:
{x > 5} x = x-3 {x > 0} is also true.

Sequences
For two adjacent statements S1 and S2:
{P1} S1 {P2}, {P2} S2 {P3}
----------------------------
{P1} S1; S2 {P3}

To find the precondition of S1; S2 with postcondition P3:


Step 1: Compute precondition of S2 using P3 -> this gives P2
Step 2: Use P2 as postcondition of S1 -> compute P1

Example: y = 3*x + 1; x = y + 3; {x < 10}


Step 1: For x = y+3 with {x < 10}: y+3 < 10 => {y < 7}
Step 2: For y = 3*x+1 with {y < 7}: 3*x+1 < 7 => {x < 2}
Precondition: {x < 2}

Selection (if-else)
Inference rule:
{B and P} S1 {Q}, {(not B) and P} S2 {Q}
-------------------------------------------
{P} if B then S1 else S2 {Q}

Example:
if x > 0 then y = y-1 else y = y+1 {y > 0}

Then clause: y = y-1 {y > 0} => precond: {y > 1}


Else clause: y = y+1 {y > 0} => precond: {y > -1}
Since {y > 1} => {y > -1}, use {y > 1} as the precondition of the whole
statement.

While Loop (Logical Pretest)


Requires finding a LOOP INVARIANT I:
Inference rule:
{I and B} S {I}
--------------------------------
{I} while B do S end {I and (not B)}
Four requirements for I to be a valid loop invariant:
1. P => I (precondition implies I)
2. {I and B} S {I} (I is preserved by loop body)
3. (I and not B) => Q (I + exit condition implies postcondition)
4. The loop terminates

If (4) is proven: called TOTAL CORRECTNESS


If (4) is ignored: called PARTIAL CORRECTNESS

Finding a Loop Invariant — Method


Compute the weakest precondition for several iteration counts (0, 1, 2, 3, ...) and look for a pattern:
Example: while y <> x do y = y+1 end {y = x}

0 iterations: precond = {y = x}
1 iteration: wp(y=y+1, {y=x}) = {y+1=x} = {y=x-1}
2 iterations: wp(y=y+1, {y=x-1}) = {y=x-2}
3 iterations: wp(y=y+1, {y=x-2}) = {y=x-3}

Pattern: {y <= x} is the loop invariant I

Verification:
1. P = I, so P => I [trivially satisfied]
2. {y<=x AND y<>x} y=y+1 {y<=x}:
wp(y=y+1, {y<=x}) = {y+1<=x} = {y<x}
{y<=x AND y<>x} => {y<x} [YES]
3. {y<=x AND NOT(y<>x)} = {y<=x AND y=x} = {y=x} => {y=x} [YES]
4. Loop terminates: y starts <= x, increments until y=x [YES]
=> I = {y <= x} is a valid loop invariant.

Program Correctness Proof Example


Proving correctness of a swap program:
Program: {x = A AND y = B}
t = x;
x = y;
y = t;
{x = B AND y = A}

Working backwards:
For y = t with {x=B AND y=A}: precond = {x=B AND t=A}
For x = y with {x=B AND t=A}: precond = {y=B AND t=A}
For t = x with {y=B AND t=A}: precond = {y=B AND x=A}

{y=B AND x=A} is the same as {x=A AND y=B} => PROVEN!

Evaluation of Axiomatic Semantics


• Powerful tool for program correctness proofs and reasoning about programs.
• Every statement type in the language needs an axiom or inference rule — difficult for
complex languages.
• Limited usefulness for describing language meaning to users or compiler writers.
• Not practical for commercial compilers.

Pragmatics (from Aaby — Introduction to Programming


Languages)
Pragmatics is concerned about the usability of the language, not its formal structure.

What Pragmatics Covers


• Usability and applicability of the language in real-world domains.
• Ease of implementation and ease of use by programmers.
• How well the language fulfills its design goals.
• Abstraction, generalization, and modularity features.

Three Key Concepts in Pragmatics


Concept Purpose
Abstraction Suppress unnecessary detail. Provides constructs to extend the language.
Reduces program complexity (e.g., functions, classes).
Generalization Apply constructs to wider classes of objects (e.g., generics, polymorphism).
Broadens applicability.
Modularity Partition programs into sections for separate compilation and reusable
libraries. Eases maintenance and understanding.

Why Pragmatics Matters


• Programs are written and read by humans but executed by computers — both requirements
must be addressed.
• Natural languages are unsuitable for programming due to imprecision.
• Humans reduce complexity through definitions, abstractions, generalizations — a language
should support these.
• Miller's Law: people can keep track of ~7 things — languages must support abstraction to
deal with complexity.
• The implementation must be faithful to the underlying computational model and be efficient.

Relationship: Syntax, Semantics, Pragmatics


Dimension Question Answered Tools / Methods
Syntax How is it written / structured? BNF, EBNF, CFG, Parse Trees
Semantics What does it mean? Attribute Grammars (static),
Operational / Denotational /
Axiomatic (dynamic)
Pragmatics How is it used? Is it practical? Language design principles, usability
analysis, real-world evaluation
Quick Reference Summary

All Topics at a Glance


Topic What it is Key Point
CFG / BNF Formal method for describing syntax LHS -> RHS; nonterminals in <>,
using production rules terminals are actual symbols
EBNF Extended BNF with [], {}, (|) for More readable than BNF; same
optional, repetition, choice expressive power
Attribute Grammar CFG + attributes + semantic Describes static semantics (type
functions + predicate functions checking, declaration rules)
Static Semantics Language rules that can be checked Cannot always be expressed in
at compile time BNF; requires attribute grammars
Pragmatics Usability, applicability, abstraction, Concerned with how well the
generalization, modularity language serves human
programmers
Operational Meaning = effect on an idealized Good for language users; depends
Semantics machine (state changes) on lower-level languages, not pure
math
Denotational Meaning = mathematical object Most rigorous; based on recursive
Semantics (function) that the construct denotes function theory; too complex for
users
Axiomatic Semantics Meaning = what can be proven Best for program correctness
using preconditions and proofs; based on predicate calculus
postconditions

You might also like