We use Z to capture the requirements for an 'intuitive' menu navigation system as a series of conjectures that should hold. We use those requirements to investigate potential algorithms. The Z formalisation enables the somewhat fuzzy requirement of 'being intuitive' to be captured precisely, analysed, and critiqued, leading to possibly new requirements, and more intuitive algorithms.
Full paper : PDF 284K
@inproceedings(SS-ZB-05b,
author = "Jemima Rossmorris and Susan Stepney",
title = "Requirements as conjectures: intuitive {DVD} menu navigation",
pages = "172-186",
crossref = "ZB-05"
)
@proceedings(ZB-05,
title = "ZB2005: Fourth International Conference of B and Z Users,
Guildford, UK, April 2005",
booktitle = "ZB2005: Fourth International Conference of B and Z Users,
Guildford, UK, April 2005",
editor = "Helen Treharne and Steve King and Martin Henson and Steve Schneider",
series = "LNCS",
volume = 3455,
publisher = "Springer",
year = 2005
)