A formal specification for Casanova, a language for computer games