Syntax and Semantics

\(\newcommand{\TirName}[1]{\text{#1}} \newcommand{\inferlab}[3]{ \let\and\qquad \begin{array}{l} \TirName{#1} \\ \displaystyle \frac{#2}{#3} \end{array} } \newcommand{\inferright}[3]{ \let\and\qquad \displaystyle \frac{#2}{#3}\TirName{#1} } \newcommand{\inferrule}[3][]{\inferlab{#1}{#2}{#3}} \newcommand{\infer}[3][]{\inferrule[#1]{#2}{#3}} \)

What questions do you have? What questions does your neighbor have?

Announcements

• Use Piazza for all course communication.
  • Energetically engage in discussions with your classmates to help each other on the learning activities — for your Class Participation score.
    • First participation assignment is your introduction
  • For course administrative things (e.g., grade issues, GitHub access issues), use private messages on Piazza to “Instructors” instead of email.

Syllabus

Highlights

• Integrity of the Course Materials
• Collaboration Policy
• Redo Policy

Review

What is a static analyzer?

An interpreter?

A verifier?

An optimizer?

Preliminaries: Programming Language Terminology

What is syntax versus semantics?

What is concrete versus abstract syntax?

What is a meta variable?

Preliminaries: Defining Syntax

JavaScripty Expressions

\[ \begin{array}{rrrl} \text{values} & v& \mathrel{::=}& n\mid b \\ \text{expressions} & e& \mathrel{::=}& n\mid b \mid x \mid\mathop{\mathit{uop}} e_1 \mid e_1 \mathbin{\mathit{bop}} e_2 \\ \text{unary operators} & \mathit{uop}& \mathrel{::=}& \texttt{-} \mid\texttt{!} \\ \text{binary operators} & \mathit{bop}& \mathrel{::=}& \texttt{+} \mid\texttt{-} \mid\texttt{*} \mid\texttt{/} \mid\texttt{\&\&} \mid\texttt{||} \mid\texttt{===} \mid\texttt{!==} \mid\texttt{<} \mid\texttt{<=} \mid\texttt{>} \mid\texttt{>=} \\ \text{numbers} & n \\ \text{booleans} & b \\ \text{variables} & x \end{array} \]

Figure 1: Syntax of JavaScripty expressions with variables, numbers, and booleans (i.e., arithmetic and logic).

A grammar is …

JavaScripty Statements

\[ \begin{array}{rrrl} \text{statements} & s& \mathrel{::=}& \texttt{;} \mid x \mathrel{\texttt{=}}e \mid s_1 \mathbin{\texttt{;}} s_2 \mid\mathbf{if}\;\texttt{(}e\texttt{)}\;s_1\;\mathbf{else}\;s_2 \mid\mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \end{array} \]

Figure 2: Syntax of JavaScripty statements with assignment, sequencing, branching, and looping.

Preliminaries: Operational Semantics

What is an operational semantics?

A semantic domain

\[ \begin{array}{rrrl} \text{stores} & \rho& \mathrel{::=}& \circ \mid\rho,x \mapsto v \end{array} \]

\[ \rho(x) \]

\[ \rho(x \leftarrow v) \]

\[ \rho[x \mapsto v] \]

Evaluating Expressions

\[ \rho \vdash e \Downarrow v \]

A judgment is …

A judgment form is …

A set of inference rules …

A derivation …