Programming-language design becomes testable when a specification predicts one outcome for every small program. MiniCalc is a conformance lab: it turns a compact contract into a grammar, typing judgments, environment traces and boundary tests. Its central program must parse one way, type as Int and evaluate to 14; any competing answer identifies a missing or inconsistent rule.
MiniCalc Specification Contract: Choices with Testable Consequences
MiniCalc is a small expression language with two types, immutable let bindings, lexical scope and strict left-to-right evaluation. Its lexer recognises integers, identifiers, Boolean literals, operators and delimiters. Its parser applies multiplication before addition, and its evaluator never converts Bool to Int. Each choice becomes an assertion that two independent implementations must satisfy.
MiniCalc feature | Chosen rule | Observable consequence |
|---|---|---|
Operator hierarchy | * before + | 2 + 3 * 4 evaluates to 14, not 20 |
Types | Int and Bool; no implicit conversions | let y:Bool = x + 3 is rejected |
Bindings | Immutable lexical let | Each let extends the environment |
Evaluation | Strict and left to right | Future extensions must preserve operand order |
Integers | Mathematical integers | The teaching language defines no overflow behaviour |
Specification boundary | No functions, mutation or division | Out-of-language forms fail at parsing |
Language Design in Programming Languages: Syntax, Types, Scope and a Worked Evaluation is the canonical overview. It covers the full design landscape: conditionals, coercion and generics, lexical versus dynamic scope, evaluation strategy, parameter passing, mutation and error models. This post has a narrower job. It treats MiniCalc as a specification-conformance lab, derives one permitted result, then tests whether two implementations would accept, reject and evaluate the same programs at the same phase. The GATE CS Exam Preparation category supplies the surrounding compiler and runtime prerequisites.
MiniCalc Grammar Conformance: One Token Stream, One AST
Consider the ambiguous grammar E ::= E + E | E * E | integer. The token stream 2 + 3 * 4 has two possible trees. Add(2, Mul(3, 4)) gives 2 + 12 = 14, while Mul(Add(2, 3), 4) gives 5 * 4 = 20. A language must remove that ambiguity through grammar, precedence declarations, parentheses or another rule. The lexer identifies integer and operator tokens; syntax decides their hierarchy.
MiniCalc uses this concrete grammar:
Program ::= Expr
Expr ::= "let" id ":" Type "=" Expr "in" Expr | Add
Add ::= Mul { "+" Mul }
Mul ::= Atom { "*" Atom }
Atom ::= integer | "true" | "false" | id | "(" Expr ")"
Type ::= "Int" | "Bool"Here * binds more tightly than +, both operators associate left, and a let body extends to the right. Concrete syntax includes tokens and punctuation. The AST keeps the essential form, such as Add(Int(2), Mul(Int(3), Int(4))). Parsing in Compiler Design: Top-Down and Bottom-Up Explained shows how a parser makes this grammar-to-AST step.

MiniCalc Type-System Conformance: Reject Before Evaluation
The type environment Gamma maps names to declared types. Integer literals are Int, Boolean literals are Bool, and names use their type in Gamma. Both e1 + e2 and e1 * e2 require two Int operands and return Int. For let x:T = e1 in e2, the initializer must have type T; the body is then checked under Gamma extended with x:T.
let x: Int = 4 in
let y: Int = x + 3 in
y * 2Start with Gamma0 = {}. Since 4 : Int, extend it to Gamma1 = {x:Int}. Under Gamma1, x + 3 : Int, so create Gamma2 = {x:Int, y:Int}. Under Gamma2, y * 2 : Int. Therefore the whole program has type Int.
Changing the second declaration to let y: Bool = x + 3 is rejected: the initializer has type Int, but the annotation requires Bool. Its tokens still match the grammar. Parsing and type checking are separate phases.
MiniCalc Operational Semantics: Reproduce the Value 14
The runtime environment rho maps names to values. MiniCalc uses lexical scope, immutable let bindings, strict left-to-right evaluation and mathematical integers. It permits no implicit conversion between Bool and Int.
Evaluate the typed program from rho0 = {}:
Evaluate
4to4, then extend the environment torho1 = {x -> 4}.Under
rho1, look upx = 4, evaluate3, and calculate4 + 3 = 7. Extend torho2 = {x -> 4, y -> 7}.Under
rho2, look upy = 7, evaluate2, and calculate7 * 2 = 14.
The program returns 14. Neither earlier environment is mutated because every let creates an extension. An independent check substitutes the immutable bindings into the final body: (4 + 3) * 2 = 7 * 2 = 14.
The type result Int and runtime value 14 answer different questions. A type describes a class of possible values; evaluation produces one value. Once type and value annotations flow over the AST, Syntax-directed translation & code optimization examples is a useful next connection.

MiniCalc Conformance Matrix: Programs Every Implementation Must Agree On
A conformance case records the source text, the phase that decides it and the only permitted outcome. This is narrower than a feature survey. These probes use only the declared MiniCalc grammar, types and immutable environments.
Six core cases are enough to expose a parser, checker or evaluator that has silently invented a different language:
2 + 3 * 4
=> AST Add(Int(2), Mul(Int(3), Int(4))); value 14
let x:Int=4 in let y:Int=x+3 in y*2
=> type Int; value 14
let y:Bool=4+3 in y
=> static rejection: initializer type mismatch
z + 1
=> static rejection: unbound identifier
true * 2
=> static rejection: operand type mismatch
let x:Int=1 in let x:Int=x+1 in x
=> type Int; value 2Cases one and six test grammar and environment boundaries together. In the shadowing case, the initializer x + 1 is checked and evaluated before the new x is added, so it reads the outer x = 1; only the body reads the inner x = 2. A result of 1 or an unbound-name error would reveal a different let rule.
Cases three to five must fail in static semantics, not at runtime. Parsing a form does not authorize evaluation; the checker must reject the program before any value environment is consulted. The required phase is part of the observable contract.
MiniCalc Specification Boundary: Reject Unowned Features
The canonical overview explains how languages may choose dynamic scope, non-strict evaluation, parameter modes, mutation and structured errors. MiniCalc does not choose among those features because its current grammar contains no functions, division, assignment, references or conditionals. A MiniCalc implementation must reject such source forms at parsing instead of borrowing behaviour from a familiar language.
The boundary prevents a teaching language from becoming accidentally underspecified. Mathematical integers are defined, so 999999999999 + 1 remains an exact integer computation rather than an overflow test. Strict left-to-right evaluation is recorded as an extension invariant, but current expressions are pure, so it does not justify claims about errors or side effects that the grammar cannot express.
MiniCalc Conformance Audit: Find the First Broken Contract
A failed MiniCalc case becomes mechanical once the first decisive contract is identified: precedence fixes the AST; the AST fixes which type rule applies; the type environment decides acceptance; and the value environment decides the result. The first disagreement names the faulty phase.
Use these six boundary checks:
Every token sequence has zero or one AST after precedence and associativity are applied.
Every accepted operator application satisfies its operand-type rule.
An annotation mismatch fails before runtime.
A let initializer uses the old environment; its body uses the extended environment.
Evaluation extends environments without mutating earlier ones.
Syntax outside the grammar is rejected, not assigned guessed semantics.
Check in 60 seconds: write the active grammar or semantic rule, build the expected AST, mark the type environment, then trace the value environment. Here 2 + 3 * 4 has one AST and value 14; the nested let program has type Int and value 14; and each invalid probe is rejected at its specified phase.
MiniCalc in Short: Add One Test Before One Feature
A language specification is complete only when independent readers derive the same AST, acceptance decision and value. MiniCalc grammar, type rules and immutable environments produce one Int value, 14, and reject forms outside the stated boundary.
Extend the conformance suite with let x:Int=5 in let y:Int=x+2 in y*3. Its expected type is Int and its value is 21. Then add one proposed feature only after writing the parse, type and evaluation outcomes that define it. For a broader guided sequence, use GATE Guidance by Sanchit Sir.




