1.1 命题逻辑：从需求句子到可判定公式
权限需求里常见一句话：“只有通过双因素认证的管理员才能删除项目。”有人把它实现成：
if (isAdmin || hasMfa) {
deleteProject();
}代码能运行，语义却已经变了。自然语言中的“只有”“除非”“当且仅当”很容易被读成不同条件。命题逻辑提供的不是符号装饰，而是一套检查翻译是否准确的方法。
命题和公式
命题是具有确定真值的陈述。在给定上下文中，它要么真，要么假：
服务器正在接受流量；请求带有有效令牌；2 + 3 = 5。
疑问句、命令句和含义未确定的句子通常不能直接当作命题。x > 3 也不是封闭命题，因为 x 尚未给值；它更适合在谓词逻辑中处理。
用命题变量 p、q 表示原子命题，再用联结词构成公式：
| 名称 | 符号 | 真值条件 | 常见代码形状 |
|---|---|---|---|
| 否定 | ¬p | p 为假 | !p |
| 合取 | p ∧ q | 二者都真 | p && q |
| 析取 | p ∨ q | 至少一个真 | p || q |
| 蕴含 | p → q | 只有 p 真且 q 假时为假 | 约束关系，不等同于 if 语句 |
| 双条件 | p ↔ q | 二者真值相同 | 两个方向的蕴含 |
形式语法告诉我们什么字符串是公式，例如：
φ ::= p | ¬φ | (φ ∧ φ) | (φ ∨ φ) | (φ → φ) | (φ ↔ φ)括号和优先级属于语法；真值属于语义。工程文档中最好保留括号，别让读者猜 ¬p ∨ q ∧ r 的结合方式。
真值赋值定义语义
一个赋值 v 为每个原子命题指定 T 或 F，复合公式的真值由联结词规则递归计算。
以蕴含为例：
p | q | p → q | ¬p ∨ q |
|---|---|---|---|
| T | T | T | T |
| T | F | F | F |
| F | T | T | T |
| F | F | T | T |
两列在所有赋值下相同，所以：
p → q ≡ ¬p ∨ q当 p 为假时，p → q 为真，这称为前件为假的情形。它表达的是一种真值约束，不自动表达现实中的因果关系、时间先后或相关性。
必要条件和充分条件
“p 是 q 的充分条件”表示：只要 p 成立，q 就成立。
p → q“p 是 q 的必要条件”表示：没有 p 就不可能有 q。
q → p回到开头的权限需求：
这里 delete 表示当前请求被允许删除，不表示删除已经实际发生。权限为真不要求用户立刻执行操作：
“只有通过 MFA 的管理员才能删除”
delete → (admin ∧ mfa)它声明管理员且通过 MFA 是删除操作的必要条件。若业务还要表达“任何满足条件的人都一定允许删除”，才补上反方向：
delete ↔ (admin ∧ mfa)权限系统通常还有资源归属、策略拒绝等条件，因此不要随意把必要条件加强成双条件。
下面只枚举两个必要条件，使用 Python 3 标准库找出开头 || 写法的反例：
from itertools import product
violations = []
for admin, mfa in product([False, True], repeat=2):
granted_by_bad_code = admin or mfa
necessary = admin and mfa
if granted_by_bad_code and not necessary:
violations.append((admin, mfa))
print(violations)
# [(False, True), (True, False)]两种反例分别是“非管理员但通过 MFA”和“管理员但未通过 MFA”。把 or 改成 and 能满足这两个必要条件；是否允许删除，还要合并其他策略。穷举四种布尔组合已经覆盖本例变量的全部赋值，但不覆盖身份数据是否可信、会话是否过期等未建模事实。
包含或与排他或
逻辑符号 ∨ 通常表示包含或：至少一个为真，二者同时为真也成立。排他或（XOR）表示恰好一个为真：
p ⊕ q ≡ (p ∨ q) ∧ ¬(p ∧ q)需求中的“用户可用密码或通行密钥登录”通常是包含或；“主节点只能位于 A 或 B，不能同时存在”才接近排他或。自然语言的“或”必须结合业务约束澄清。
三种重要的公式性质
对于公式 φ：
- 永真式：每个赋值都使
φ为真，例如p ∨ ¬p； - 矛盾式：没有赋值使
φ为真，例如p ∧ ¬p； - 可满足式：至少存在一个赋值使
φ为真。
可满足不等于永真。p ∧ q 可满足，但只有二者都真时成立。
还有两个容易混淆的关系：
φ ≡ ψ 所有赋值下真值相同（逻辑等价）
Γ ⊨ φ 每个满足前提集合 Γ 的赋值也满足 φ（语义蕴涵）例如：
{p → q, p} ⊨ q这不是说 q 与前提等价，而是说任何同时满足两个前提的赋值都不能让 q 为假。
从需求翻译公式的步骤
需求：
若部署进入生产环境，则必须完成审批和安全扫描；紧急变更可以没有普通审批，但仍必须扫描。
先定义原子命题：
p: 部署到生产
a: 完成普通审批
s: 安全扫描通过
e: 属于紧急变更再拆成独立约束：
p → s
(p ∧ ¬e) → a
e → p // 若业务定义紧急变更一定是生产变更不要急着压成一条“聪明”的公式。多条命名清楚的约束更容易评审，也便于 SAT/SMT 工具指出是哪条冲突。
逻辑运算与程序执行不完全相同
在纯布尔值上，p ∧ q 和 q ∧ p 等价；在有副作用或错误的程序中，调换操作数可能改变行为：
user != null && user.isActive()Java 的 && 短路求值，先检查 user != null。交换顺序会先解引用 user，可能抛出异常。数据库 SQL 还存在 NULL 导致的三值逻辑，不能直接把所有 WHERE 条件当作经典二值命题公式重写。
使用逻辑等价优化代码前，应确认表达式求值是总定义、无副作用，且所处语言的真值体系相同。
上述 Java 行为由 JLS 21 §15.23 定义。还要区分原始 boolean 与可空 Boolean：后者在自动拆箱时也可能抛出异常。
完成检查
把以下需求翻译成公式，并写出原子命题定义：
- 只有负责人或管理员可以关闭工单；
- 发布必须通过测试，除非发布被取消；
- 主副本和备用副本至少有一个可用，但不能同时承担主角色；
- 若请求既没有令牌也不在允许网络内，则拒绝请求。
对每条公式再找一个“自然语言看似相近、逻辑却不同”的反例。