Programming Languages Chapter 3

Describing Syntax and Semantics

• Programming language descriptions must cater to various groups: evaluators, implementers, and programmers.
• Syntax refers to the structure/form of code, while semantics involves the meaning or effect of that code.
• Example of syntax: while (boolean_expr) statement (Java).
• Semantics of the while construct dictates its execution based on the truth value of boolean_expr.

Unambiguous Grammar

• Defined for control structures like if-then-else.
• An unambiguous grammar guarantees a single parse tree for given input to avoid confusion.

Extended Backus-Naur Form (EBNF)

• EBNF enhances BNF by allowing optional parts, alternatives, and repetitions.
• Syntax examples:
  • Optional: -> ident [()]
  • Alternatives: -> (+|-) const
  • Repetitions: -> letter {letter|digit}

Static Semantics

• Some language characteristics are challenging to express in BNF, like type compatibility rules.
• Example: A floating-point type cannot be assigned to an integer variable, but the reverse is permissible.

Attribute Grammars

• Define rules where attributes of nonterminals are determined using functions.
• Attributes can be synthesized (calculated from children) or inherited (passed down from parent).
• Example: actual_type stores the type of a variable, while expected_type indicates the anticipated type.

Operational Semantics

• Provides a method to understand program behavior through a virtual machine simulation.
• Informally useful in language manuals; formally complex in academic definitions.
• Levels:
  • Natural operational semantics: Focuses on end results.
  • Structural operational semantics: Examines program meaning through detailed structural analysis.

Axiomatic Semantics

• Uses assertions (preconditions and postconditions) to define relationships between variables during execution.
• Example format: {P} statement {Q} where P is a precondition and Q a postcondition.
• Weakest precondition is the least restrictive that ensures the postcondition holds.

Program Proof Process

• Initiates with the program’s postcondition and computes backwards through the program statements to verify correctness.
• If input specifications satisfy the derived precondition, the program is validated.

Axiomatic Semantics: Assignment

• Assignment statements have a defined weakest precondition calculated by substituting the variable with its expression, denoted as P = Qx->E.