creators_name: Leuschel, Michael creators_name: Samia, Mireille creators_name: Bendisposto, Jens creators_name: Samia, Mireille creators_id: leuschel@cs.uni-duesseldorf.de type: conference_item datestamp: 2008-11-04 09:22:45 lastmod: 2010-04-19 15:05:51 metadata_visibility: show title: Easy Graphical Animation and Formula Visualisation for Teaching B ispublished: pub subjects: deploy_tooldev subjects: deploy_tooldev_modela subjects: deploy_training full_text_status: public pres_type: paper abstract: ProB is being used for teaching the B-method. In this paper, we present two new features of ProB that we have introduced while teaching B. One feature allows a student (or an expert user) to graphically visualise any predicate as a tree. The underlying algorithm can deal with undefined subformulas and tries to provide useful feedback even for existentially quantified formulas which are false. This feature is especially useful to inspect unexpected invariant violations or operations which are unexpectedly enabled or disabled. The other feature enables a student or lecturer to easily and quickly write custom graphical state representations, to provide a better understanding of the model. With this method, one simply has to assemble a series of pictures and to write an animation function in B itself, which stipulates which pictures should be shown where depending on the current state of the model. As an additional side-benefit, writing the animation function in B itself is a good exercise for students. date: 2008 date_type: published event_title: The B Method : From Research to Teaching event_location: Nantes, France event_dates: June 16, 2008 event_type: workshop refereed: TRUE citation: Leuschel, Michael and Samia, Mireille and Bendisposto, Jens and Samia, Mireille (2008) Easy Graphical Animation and Formula Visualisation for Teaching B. In: The B Method : From Research to Teaching, June 16, 2008, Nantes, France. document_url: http://deploy-eprints.ecs.soton.ac.uk/47/1/teaching_animation.pdf