Willem van den Ende
4cdb048dfc
- 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)
50 lines
1.3 KiB
Plaintext
50 lines
1.3 KiB
Plaintext
-- allium: 3
|
|
|
|
-- allium: damage-and-health
|
|
|
|
------------------------------------------------------------
|
|
-- Rules
|
|
------------------------------------------------------------
|
|
|
|
rule DamageReducesHealth {
|
|
when: Character.dealDamage(attacker, target, damage)
|
|
requires: attacker.name != target.name
|
|
requires: target.status = alive
|
|
ensures: target.health.value = max(0, target.health.value - damage)
|
|
ensures:
|
|
if max(0, target.health.value - damage) = 0:
|
|
target.status = dead
|
|
else:
|
|
target.status = alive
|
|
}
|
|
|
|
rule SelfDamageForbidden {
|
|
when: Character.dealDamage(attacker, target, damage)
|
|
requires: attacker.name = target.name
|
|
ensures:
|
|
target.health.value = target.health.value
|
|
target.status = target.status
|
|
}
|
|
|
|
rule DeadCannotTakeDamage {
|
|
when: Character.dealDamage(attacker, target, damage)
|
|
requires: target.status = dead
|
|
ensures:
|
|
target.health.value = target.health.value
|
|
target.status = dead
|
|
}
|
|
|
|
------------------------------------------------------------
|
|
-- Invariants
|
|
------------------------------------------------------------
|
|
|
|
invariant HealthNonNegative {
|
|
for c in Characters:
|
|
c.health.value >= 0
|
|
}
|
|
|
|
invariant DeathAtZeroHealth {
|
|
for c in Characters:
|
|
c.health.value = 0 implies c.status = dead
|
|
}
|