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 )