Usability is the most important featureof a computer program from the user's point of view. Even if various techniques for evaluating usability have been proposed, formal methods are still lacking. A good indication of program usability is given by the agreement between the mental model of the system, as conceived by the user, and the model of the user, as understood by the designer and implemented in the system. We extend here the visual sentence theory we have developed in the last years by introducing the concept of relation system. This provides a means for describing both the user's and the program's models. Basedon this formalism, we can also define some measurable properties for usability, and develop experimental protocols for their measurement.