表达式语义规范

表达式是具有静态类型并在运行时产生值的计算。语句只产生完成效果；控制结构只有出现在值位置并满足路径规则时才成为表达式。

基本判断

Γ ⊢ e : T 表示表达式 e 在静态环境 Γ 中类型为 T。表达式求值记为 ⟨e, Σ⟩ ⇓ ⟨v, Σ'⟩，其中 v 必须满足 T。

求值顺序

• 操作数与实参按源码从左到右求值；
• && 与 || 短路；
• if 只求值选中的分支；
• switch 被匹配值只求值一次，case 不 fallthrough；
• assignment 在右侧成功求值后才更新目标。

控制表达式

String result = if enabled {
    break "enabled"
} else {
    break "disabled"
}

表达式上下文要求每条可正常完成的路径产生 break value。Return 和 Throw 属于不正常完成，不需要额外值。每个 switch 还必须在静态阶段证明模式穷尽。编译器计算所有 Value 完成结果的共同静态类型；不存在唯一类型时拒绝程序。

无隐式 Null

缺失 else 或耗尽 for 不会自动得到 null。switch 的未匹配路径由穷尽检查在编译期排除；其他控制表达式必须补全路径或显式返回 nullable 类型。

调用和构造

构造调用与普通函数调用都先解析命名参数，并按源码顺序求值。value 参数产生逻辑独立值，class 参数保留对象身份。默认参数在被调用函数声明环境中求值，当前草案要求其为编译期常量。

错误

静态错误包括：使用 Void 值、路径缺少结果、条件非 Boolean、调用歧义和不安全赋值。运行时异常不改变表达式的静态类型，而以 Throw 完成结果传播。