refactor(story2): immutable dealDamage, reference guard, negative damage validation, spec precision

- dealDamage returns new Character instead of mutating in-place
- SelfDamageForbidden uses reference equality (this === target)
- Negative damage throws at the boundary
- Removed duplicate Health.maxHealthForLevel (Level.ts is source of truth)
- Allium spec uses max(0, ...) for health floor precision
- New property: NegativeDamageForbidden (11 total properties)
This commit is contained in:
2026-06-13 15:44:46 +01:00
parent a9c20a5f1b
commit 4cdb048dfc
4 changed files with 62 additions and 36 deletions
+2 -2
View File
@@ -10,9 +10,9 @@ rule DamageReducesHealth {
when: Character.dealDamage(attacker, target, damage)
requires: attacker.name != target.name
requires: target.status = alive
ensures: target.health.value = target.health.value - damage
ensures: target.health.value = max(0, target.health.value - damage)
ensures:
if target.health.value - damage <= 0:
if max(0, target.health.value - damage) = 0:
target.status = dead
else:
target.status = alive