We have been engaged in research towards designing a software system called LOZ for learning the object oriented formal specification notation Object-Z. Initially, we conducted a survey to analyse the effectiveness of traditional methodologies for learning Z notation. In LOZ, the semiformal model UML is used in the intermediate phase between informal textual description and formal Object-Z description. We also employ a refinement unit that produces code from the specification. Based on the cognitive apprenticeship approach, we employ a four-phase instructional model in our system. Persuading the learners to be partially responsible for their own model and allowing them to decide their own levels of control over the learning process are key features of our system.