1.0.P6 Postconditions

Pattern 6 · Promise, then repair

When you want a Tag to guarantee something about the finished Agent. Postconditions inspect the product after everything applied.

class Wizard(Tag):

    @Post
    def Has_Spellbook(agent):
        assert agent.spellbook is not None


newt = Character("Newt")
newt.spellbook = None

try:
    Wizard(newt)
except Postcondition.Has_Spellbook:
    pass                                # the Tag stays; Newt is defective

assert newt in Wizard                   # a member
assert not newt                         # whose promise is broken
assert newt in ~Wizard                  # waiting in the repair queue

for broken in ~Wizard:                  # the repair loop
    broken.spellbook = []

assert newt                             # sound again
assert newt in list(Wizard)             # back in the working population

This is the factory rule: a bad product is not melted back to materials. It is flagged, repaired, or thrown away (del Wizard[newt]).

if agent: reads "are this agent's promises holding". When you need the name of the broken one, Contract.Display(agent) or f"{agent:contract}" prints them.

Necessary to enter, necessary to stay. Stack @Pre and @Post on one function and it is both: a gate at the door and a promise kept after.

class Elf(Tag):

    @Pre
    @Post
    def Alive(agent):
        return agent.alive


ghost = Character("Ghost")
ghost.alive = False

try:
    Elf(ghost)
except Precondition.Alive:
    pass                                # not alive: cannot become an Elf

ari.alive = True
Elf(ari)
ari.alive = False                       # an Elf who died is a broken Elf
assert ari in ~Elf

Being alive is necessary to be an Elf, not sufficient: other living things are not Elves. That is the difference between a condition and a Tag.

When the claim reads better as one necessity than as two checks, write @Requirement instead of the pair. It means exactly the same thing:

class Elf(Tag):

    @Requirement
    def Alive(agent):
        return agent.alive

It still fails under two names, because you repair the two differently: Precondition.Alive is someone who may not come in, Postcondition.Alive is an Elf already in and now broken.

Watch out. A Shape should promise at least what its Base promised. Use @Post @Underlay and return base() and .... Overriding a Base's promise without it weakens the contract; TopKit allows it and warns.