Willem van den Ende
fc2cf73b34
- Allium spec: damage-and-health.allium - 5 fast-check properties: damage reduces health, health non-negative, death at zero, self-damage forbidden, dead cannot take damage - Character.createWithHealth factory for testing with arbitrary health - Character.dealDamage(target, damage) method
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 = target.health.value - damage
|
|
ensures:
|
|
if 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
|
|
}
|