This tutorial series assumes knowledge of Java and the working environment is Eclipse.
This tutorial series assumes no knowledge of Java and the working environment is primarily Eclipse and partly Android Studio.
This tutorial series assumes no knowledge of Java and the working environment is Eclipse.
App Development Pattern: Single Button Manipulating a Single Model Object
App Development Pattern: Multiple Buttons Sharing a Single Model Object
Model Development Pattern: Declaring Attributes with Reference Types
Model Development Pattern: Declaring Attributes with Array-Referenced Types
Study Notes:
across
as Loop Instructions (23:46)
across
as Boolean Expressions (21:28)
add
- Debugging Precondition (30:45)
add
- Testing Postcondition (35:16)
detachable
? [Supplier] (39:52)
detachable
? [Client] (24:49)
celebrate
(18:57)
NOTES: Follow each tutorial video with its associated section in this document, which also contains links to the corresponding tutorial videos.
Follow this tutorial video with this document.
Follow this tutorial video with Section 3 of this lab session.
Follow this tutorial video with this document.
Follow this tutorial video with Section 2 of this lab session.
Written ETF Tutorial: A Simple Banking System
Script for Regression Testing of Acceptance
Oracle Program (Linux executable) for the Bank Example
This tutorial series assumes an installation of Rodin 3.6 (see http://www.event-b.org/install.html and here for details).
Those with active EECS accounts may use the remote lab to launch the Rodin tool.
This tutorial series assumes an installation of TLA+ (see https://lamport.azurewebsites.net/tla/toolbox.html and here for details).
Those with active EECS accounts may use the remote lab to launch the Rodin tool.