zhanlang Language Specification

Version: v0.1

Date: 2026-10-17

This document is the normative definition of zhanlang. Where an implementation conflicts with this document, this document wins; anything left undefined here is “unspecified” and an implementation may choose freely, but must document its choice.

中文译文见 spec.zh-CN.md（非规范，以本英文版为准）。

Table of contents

1. Lexical structure
2. Syntax
3. Type system
4. Intent blocks (spec)
5. Effect system
6. Verification tiers
7. Standard library (minimal)
8. Examples
9. Conformance

1. Lexical structure

1.1 Comments

• // to end of line is a line comment.
• /* to the nearest */ is a block comment; it does not nest.

1.2 Identifiers and keywords

• Identifier: [A-Za-z_][A-Za-z0-9_]*.

• Keywords (reserved; cannot be used as identifiers):

  module type record enum fn spec pre post examples if else match is old modifies events let return todo true false private Int Float Bool String

• Case-sensitive. By convention types and constructors start with an uppercase letter and variables and functions with a lowercase letter, but the grammar does not enforce this.

1.3 Literals

• Integer: [0-9]+, type Int (v0.1 uses 64-bit signed integers; overflow behavior is implementation-documented).
• Float: [0-9]+ "." [0-9]+, type Float.
• String: "..."; the only escapes are \", \\, \n, \t; type String.
• Boolean: true, false.

1.4 Operators and delimiters

• Operators: + - * / % == != < <= > >= && || !
• Delimiters: ( ) { } [ ] < > , . : -> => ? _

2. Syntax

2.1 Program structure

program     := module_decl? decl*
module_decl := "module" ident
decl        := type_decl | enum_decl | fn_decl

A file is a module; module may be omitted, in which case the module name is the file name.

2.2 Type declarations

type_decl := "type" ident "=" type
enum_decl := "enum" ident "{" variant ("," variant)* "}"
variant   := ident ("(" ident ":" type ("," ident ":" type)* ")")?

2.3 Function declarations

fn_decl    := "private"? "fn" ident type_params? "(" params? ")" ("->" type)? effects? body_part? block
type_params:= "<" ident ("," ident)* ">"
params     := param ("," param)*
param      := ident ":" type
effects    := effect+
effect     := "io" | "async" | "random" | "time"
body_part  := spec_block | trusted_note
trusted_note := "trusted" "(" string ")"

Visibility and its relation to spec are described in §4.4.

2.4 spec blocks

spec_block := "spec" "{" spec_item* "}"
spec_item  := "pre" expr | "post" expr
            | "modifies" ident ("," ident)*
            | "examples" "{" example* "}"
example    := expr ("==" expr | "is" pattern)

2.5 Statements and blocks

block := "{" stmt* expr? "}"
stmt  := "let" ident (":" type)? "=" expr ";"
       | "return" expr? ";"
       | expr ";"

The value of a block is its trailing expression; without one, the block yields () (unit). v0.1 does not treat unit as an ordinary type; it exists only for return;.

2.6 Types

type     := "Int" | "Float" | "Bool" | "String"
          | ident type_args?
          | type "?"
type_args:= "<" type ("," type)* ">"

T? is sugar for Option<T>.

2.7 Expressions

expr       := if_expr | match_expr | or
if_expr    := "if" expr block "else" block
match_expr := "match" expr "{" match_arm ("," match_arm)* "}"
match_arm  := pattern "=>" expr
or         := and ("||" and)*
and        := cmp ("&&" cmp)*
cmp        := add (("=="|"!="|"<"|"<="|">"|">=") add)*
add        := mul (("+"|"-") mul)*
mul        := unary (("*"|"/"|"%") unary)*
unary      := "-" unary | "!" unary | postfix
postfix    := primary ("(" expr ("," expr)* ")" | "." ident | "[" expr "]")*
primary    := literal | ident | "(" expr ")" | "todo"
            | ident "{" field ("," field)* "}"      // 记录字面量
field      := ident ":" expr

Precedence, low to high: || → && → comparison → addition/subtraction → multiplication/division/remainder → unary ! - → postfix (call/field/index) → primary.

ident "(" ... ")" covers ordinary function calls as well as constructors (Ok(x), Some(x), enum variants).

2.8 Patterns

pattern := "_" | literal | ident ("(" pattern ("," pattern)* ")")?

Patterns appear in match arms and in is assertions. ident(p1, ...) is a constructor pattern; a bare ident is a wildcard binding.

3. Type system

3.1 Classification

• Primitive types: Int, Float, Bool, String.
• Optional: T?.
• Parameterized types: List<T>, Map<K, V>, Result<T, E>.
• Records: record.
• Enums: enum.
• Type aliases: type X = T.

3.2 Rules

• Static and strongly typed, no implicit conversion. Int and Float must be converted explicitly: Int has to_float() -> Float and Float has to_int() -> Int (truncating toward zero). Round-trip precision loss from floating-point representation is implementation-documented and not guaranteed.
• Generics are invariant, with no bounds.
• A T? must be unwrapped before it is used as T; the only ways to unwrap are match and is-assertion binding.
• The legal constructors of Result<T, E> are Ok(T) and Err(E).

3.3 Null safety

Any direct field access or operation on T? is a type error. The only way to unwrap is match:

match u.age {
  Some(a) => a >= 18
  None => false
}

4. Intent blocks (spec)

4.1 Components

• pre expr: a condition that must hold on entry.
• post expr: a condition that must hold on return; result names the return value.
• examples: input/output examples, each of the form expr == expr or expr is pattern.
• modifies x, ...: declares the external state this function may write (frame constraint).

4.2 Expression domain

spec expressions are pure by default. The following special forms are allowed:

• old(expr): the value of expr at function entry; allowed only in post.
• events: a compiler-maintained ghost event history; allowed only in post.
• is: a pattern-match assertion, e.g. result is Ok, result is Err(e), u.age is Some(a).

old, events, and is are not allowed in a function body; side-effecting calls such as io are not allowed in spec.

4.3 spec self-check (at construction time, mandatory)

The compiler performs the following checks on every spec; any failure rejects compilation:

1. Non-vacuity. A post must not be a tautology. At minimum post true and post x == x are rejected; more general tautology detection is best-effort and a miss is not an error.
2. Reachability. For a post of the form match result { ... }, every variant must be reachable when pre holds; a branch that obviously contradicts pre (e.g. Err(InvalidPrice) => price <= 0 while pre price > 0) is rejected. Full reachability is undecidable; v0.1 detects only obvious contradictions.
3. Example consistency. Each example’s inputs must satisfy pre, and its expected output must not contradict post. This is decided statically within the pure subset and at runtime in the checked tier otherwise.
4. Reference legality. Every identifier in spec must be a parameter, result, a built-in pure function, or a declared pure function that carries its own spec; undefined identifiers are rejected.

4.4 Visibility and omitting spec

• Top-level functions are public (externally visible) by default.
• Public functions must carry a spec.
• private functions may carry a spec or omit it; omission requires a trusted("reason") annotation.
• trusted is allowed only on private functions.

5. Effect system

Functions are pure by default. Functions that need external capabilities declare effects:

• io: reads or writes external state.
• async: suspension and concurrency.
• random: non-determinism.
• time: dependence on the clock.

Effects propagate up the call graph: a pure function calling a function that declares io is a type error. Effects are part of a function’s type.

6. Verification tiers

Construction-time verification has three tiers; downgrading must be explicit:

The downgrade order is fixed: try verified, fall back to checked. Silent downgrade is not allowed. No tier changes the meaning of the spec, only when verification happens.

7. Standard library (minimal)

v0.1 guarantees only the following built-ins; everything else is unspecified. First-class functions and higher-order operations such as map / filter are not guaranteed in v0.1.

• Int: to_float() -> Float.
• Float: to_int() -> Int (truncating toward zero).
• String: len -> Int, contains(String) -> Bool, starts_with(String) -> Bool, ends_with(String) -> Bool.
• List<T>: len -> Int, is_empty() -> Bool, get(Int) -> T?.
• Map<K,V>: len -> Int, has(K) -> Bool, get(K) -> V?.
• Option<T>: constructors Some / None.
• Result<T,E>: constructors Ok / Err.
• events: a ghost sequence, len -> Int, contains(Event) -> Bool.

8. Examples

Runnable examples live in examples/. Two core ones:

fn max(a: Int, b: Int) -> Int
  spec {
    post result >= a
    post result >= b
    post result == a || result == b
    examples {
      max(1, 2) == 2
      max(5, 5) == 5
    }
  }
{
  if a >= b { a } else { b }
}

fn register(email: String, password: String) -> Result<UserId, RegError>
  io
  spec {
    pre email.contains("@")
    pre password.len >= 8
    modifies db
    post result is Ok || result is Err(EmailTaken)
    examples {
      register("a@b.com", "abcdefgh") is Ok
    }
  }
{
  todo
}

9. Conformance

An implementation is conformant if and only if:

1. every program under examples/ passes parsing, type checking, and spec self-check;
2. every program under conformance/reject/ is rejected for the annotated reason;
3. the checked tier catches calls that violate pre / post at runtime;
4. calling a trusted function from outside its module is rejected.

The conformance cases are maintained alongside the repository and are the sole judge of conformance. See conformance/README.md.