at-m42:casestudies:cs04
Differences
This shows you the differences between two versions of the page.
Both sides previous revisionPrevious revisionNext revision | Previous revision | ||
at-m42:casestudies:cs04 [2009/04/15 09:02] – eechris | at-m42:casestudies:cs04 [2011/01/14 12:59] (current) – external edit 127.0.0.1 | ||
---|---|---|---|
Line 774: | Line 774: | ||
game.addItem(item) | game.addItem(item) | ||
actual = game.pickupItem(item.id, | actual = game.pickupItem(item.id, | ||
- | println actual | ||
} | } | ||
Line 782: | Line 781: | ||
} | } | ||
</ | </ | ||
- | ===== Exercises ===== | + | Since Groovy' |
+ | |||
+ | This is an example of a //loop variant//. although it does not concern us here, loop invariants are widely used in formal approaches to software development where proof of correctness is important. For our purposes, we just need to demonstrate that if we start at some object and follow a sequence of object links, then we arrive back at the same object. The object diagram of Figure 4 illustrates this. | ||
+ | |||
+ | {{: | ||
+ | |||
+ | **Figure 4**: An Item-Player loop invariant. | ||
+ | |||
+ | The figure shows that if we start from a given '' | ||
+ | <code groovy> | ||
+ | // class: Game | ||
+ | private void checkItemCarrierLoopInvariant(String methodName) { | ||
+ | def items = inventory.values().asList() | ||
+ | |||
+ | def carriedItems | ||
+ | |||
+ | def allOK = carriedItems.every { item -> | ||
+ | item.carrier.inventory.containsKey(item.id) | ||
+ | } | ||
+ | |||
+ | if (! allOK ) { | ||
+ | throw new Exception(" | ||
+ | } | ||
+ | } | ||
+ | </ | ||
+ | |||
+ | Since the violation of an invariant indicates that a serious error has occurred, we terminate the system by throwing an '' | ||
+ | |||
+ | As before, we only check methods that are likely to cause a violation. In this case it is just the method '' | ||
+ | |||
+ | <code groovy> | ||
+ | // class: Game | ||
+ | // ... | ||
+ | if (player.inventory.size() < Player.LIMIT) { | ||
+ | player.pickUp(item) | ||
+ | this.checkItemCarrierLoopInvariant(' | ||
+ | message | ||
+ | } | ||
+ | else { | ||
+ | message | ||
+ | } | ||
+ | // ... | ||
+ | </ | ||
+ | |||
+ | Before we finish, we must create at least one unit test to check that the expected '' | ||
+ | |||
+ | One solution is to create a '' | ||
+ | <code groovy> | ||
+ | class MockPlayer extends Player { | ||
+ | |||
+ | Boolean pickUp(Item item) { | ||
+ | if (! inventory.containsKey(item.id)) { | ||
+ | // | ||
+ | // Normal behviour commented out | ||
+ | // inventory[item.id] | ||
+ | item.pickedUpBy(this) | ||
+ | return true | ||
+ | } | ||
+ | else { | ||
+ | return false | ||
+ | } | ||
+ | } | ||
+ | |||
+ | } | ||
+ | </ | ||
+ | |||
+ | We create a '' | ||
+ | |||
+ | <code groovy> | ||
+ | // class: GameTest | ||
+ | void testCheckItemCarrierLoopInvariant() { | ||
+ | def mockPlayer | ||
+ | email : ' | ||
+ | game.registerPlayer(mockPlayer) | ||
+ | game.addItem(book) | ||
+ | game.addItem(satchel) | ||
+ | |||
+ | try { | ||
+ | game.pickupItem(book.id, | ||
+ | fail(' | ||
+ | } catch (Exception e) { | ||
+ | // ignore exception | ||
+ | } | ||
+ | } | ||
+ | </ | ||
+ | |||
+ | Note that the method '' | ||
+ | |||
+ | Happily all the tests in the '' | ||
+ | |||
at-m42/casestudies/cs04.1239786121.txt.gz · Last modified: 2011/01/14 12:47 (external edit)