Jackie's Tutorials

Roadmap

• Procedural and Object-Oriented Programming in Java
  • Use of the ANTLR4 Parser Generator to Develop a Compiler
  • Java from Scratch: from Procedural to Object-Oriented and Mobile Programming
  • Java from Scratch: from Procedural to Object-Oriented Programming
  • Developing an Apple Refurbished Store App
  • Developing a Birthday Book App
  • Java Collections
• Eclipse
• Object Oriented Programming in Android Studio
  • BMI Calculator App (Model Pattern: Single Button, Single Model Object)
  • Counter App (Model Pattern: Multiple Buttons, Single Model Object)
  • Point and PointeCollector Model Classes (Model Pattern: Attributes with Reference Types)
  • Student Management System (Model Pattern: Attributes with Array-Referenced Types)
• Software Design
  • Introductory Tutorial: Eiffel Language/Method/Tool for Design (Fall 2020)
  • Use of Eiffel Studio for DbC and TDD (Summer 2015)
  • Generic Parameters and the Iterator Pattern
  • Information Hiding and the Iterator Pattern
  • Eiffel Testing Framework (ETF): a Framework for Testing Design
  • Design Patterns: Composite and Visitor
• Formal Methods for System Development
  • Introduction to the Rodin Platform for Formal Specifications
  • Introduction to the TLA+ Toolbox for Formal Specifications

Procedural and Objected Oriented Programming in Java

•  Use of the ANTLR4 Parser Generator to Develop a Compiler ( iPad Notes)

  This tutorial series assumes knowledge of Java and the working environment is Eclipse.

  • Part 1: Installation of antlr and grun, Setting Up Eclipse Projects, References (09:55)
  • Part 2: What a Parser Generator Is, Specifying Tokens and Grammmars, Using grun to Test Grammars (45:41)
  • Part 3: Design/Implementation of Model Classes, Visiting ANTLR Parse Trees to Build Model Objects, Adding Labels to Grammar (42:27)
  • Part 4: Implementing Two Visitor Classes for Transforming Parse Trees to Program/Expression Objects (1:03:08)
  • Part 5: Creating a Console Application, Run Configuration, Exporting Project as Runnable JAR (48:46)
  • Part 6: Syntax (Grammatical) Errors vs. Semantic Errors, Error Handing by Adding a Listener (25:38)
  • Part 7: Adding Semantic Actions to Each Production Alternative, Comparison: Visitor vs. Action (1:00:10)

•  Java from Scratch: from Procedural to Object-Oriented and Mobile Programming ( iPad Notes)

  This tutorial series assumes no knowledge of Java and the working environment is primarily Eclipse and partly Android Studio.

  • Week 1: Separation of Concerns - Model, Console Apps, Unit Testing
    1. Part A: Setting Working Environment (Github, Eclipse, Remote Labs) (40:10)
    2. Part B: Setting the Java Perspective (15:33)
    3. Part C: Console Applications (23:27)
    4. Part D: Utility Classes (24:24)
    5. Part E: JUnit Tests (21:58)
    6. Part F: Separation of concerns (using packages) (13:30)
  • Week 2: Use of Debugger and Introduction to Conditionals
    7. Part A: Arithmetic Sequence - Console Applications (41:23)
    8. Part B: Arithmetic Sequence - Utility Methods & JUnit Tests (27:10)
    9. Part C: Debugger - Executing Code in Slow Motion (Step Over/Into/Out) (17:00)
    10. Part D: Using Debugger in Eclipse (Step Over) (13:17)
    11. Part E: Using Debugger in Eclipse (Step Into/Out) (24:01)
    12. Part F: Single If-Statement with Overlapping Conditions (11:41)
    13. Part G: Multiple If-Statements with Non-Overlapping Conditions (11:52)
  • Week 3: Exploration of Logical Operations and Nested Conditionals
    14. Part A: Setting Up, Reviewing the Grade Example (09:17)
    15. Part B: V1 - Single If-Stmt, Overlapping Conditions (18:11)
    16. Part C: V2 - Multiple If-Stmts, Disjoint Conditions (10:59)
    17. Part D: V3 - Multiple If-Stmts, Disjoint Conditions (18:13)
    18. Part E: Specifying Ranges - Conjunction vs. Disjunction (25:22)
    19. Part F: Nested If-Statements (30:00)
    20. Part G: Helper Method, Using Disjunction, Negation (28:54)
  • Week 4: Introducing Loops to Patternize Repetitive Actions
    21. Part A: Motivating Example of Grade Calculation (with duplicates) (28:24)
    22. Part B1: Introducing for-Loops in Java (18:03)
    23. Part B2: Using for-Loops in Console Applications (25:36)
    24. Part C: Using while-Loops in Console Applications (16:03)
    25. Part D: Utility Method with Loops (a fixed number of iterations) (30:35)
    26. Part E: Utility Method with Loops (an indefinite number of iterations) (13:33)
  • Week 5: Introducing Arrays: Syntax, Applications, and Tracing
    27. Part A1: Tracing while-Loops on Paper (16:57)
    28. Part A2: Tracing while-Loops on Debugger (15:07)
    29. Part B: Using while-Loops in Console Applications (30:22)
    30. Part C1: Arrays: Initializer, Memory, Indexing (30:14)
    31. Part C2: Arrays: Creating a New Array Object (12:50)
    32. Part D1: Example: Calculating Intermediate Sums (19:12)
    33. Part D2: Tracing: Calculating Intermediate Sums (24:52)
  • Week 6: Classes, Attributes, Constructors, Accessors, Mutators, Method Invocations
    34. Part A: Resources, Creating a Class (08:41)
    35. Part B1: Class, Attributes, Default Constructor (19:40)
    36. Part B2: Tracing Object Creations using Debugger (16:41)
    37. Part C1: Tracing Object Creations on Debugger (21:49)
    38. Part C2: Tracing Object Creations on Paper (28:17)
    39. Part C3: Invoking a Helper Constructor (08:53)
    40. Part D1: Defining & Invoking Accessors and Mutators (23:20)
    41. Part D2: Syntax: Accessor Methods vs. Mutator Methods (06:08)
    42. Part D3: Tracing & Visualizing Method Invocations (23:02)
  • Week 7: Reference Aliasing and Reference-Typed, Single-Valued Attributes
    43. Part A1: Reference Aliasing - Copying an Object Address (30:51)
    44. Part A2: Reference Aliasing - Swapping Object Addresses (11:54)
    45. Part B1: Example: A Member's Trainer - Accessors and Mutators (21:13)
    46. Part B2: Example: A Member's Trainer - Unit Testing (13:48)
    47. Part B3: Example: A Member's Trainer - Visualization and Tracing (31:27)
    48. Part C1: Example: A Member's Facilities - Initial Coding and Written Notes (20:47)
  • Week 8: Reference Aliasing and Reference-Typed, Multi-Valued Attributes
    49. Part C2: Recap, Resources, Setting Up (10:37)
    50. Part C3: Coding & Testing - Adding Facility and Accessing Number of Facilities (23:48)
    51. Part C4: Tracing & Visualizing - Additions of Facility Objects (29:19)
    52. Part C5: Anonymous Objects and Overloaded Methods (17:10)
    53. Part D1: Coding & Testing - Accessor method getPaymentDue (13:57)
    54. Part D2: Tracing & Visualizing - Accessor Method getPaymentDue (16:57)
    55. Part E1: Coding & Testing - Retrieval and Change of Facility (24:29)
    56. Part E2: Tracing & Visualizing - Retrieval and Change of Facility (25:00)
  • Week 9: Application of OOP in Mobile Computing (Android Studio)
    57. Part A1: Greeting App - Creating an Empty Activity (09:11)
    58. Part A2: Greeting App - GUI Design (activity_main.xml) (31:43)
    59. Part A3: Greeting App - Attaching Controller (MainActivity) Methods to GUI Components (23:44)
    60. Part A4: Greeting App - Event-Driven Programming (EDP) (11:56)
    61. Part B1: Counter App - GUI Design (activity_main.xml) (20:37)
    62. Part B2: Counter App - Attaching Controller (MainActivity) Methods to GUI Components (22:10)
    63. Part B3: Counter App - Tracing EDP and Model-View-Controller (MVC) Pattern (18:35)
    64. Part B4: Counter App - JUnit Tests and Debugger in Android Studio (09:19)
  • Week 10: Two-Dimensional Arrays (Part I: Milelage Calculation)
    65. Part A: Problem - Calculating Mileage of Travel (13:39)
    66. Part B1: Version 1a - Storing Distances Table & Itinerary Cities (17:32)
    67. Part B2: Version 1a - Explicit Checks on Dep/Dst Cities (24:10)
    68. Part B3: Version 1b - Implicit Checks on Dep/Dst Cities (22:48)
    69. Part C1: 2D Arrays - Initialization (with Initializer), Lengths, Indexing (21:54)
    70. Part C2: 2D Arrays - Initialization (with new), Indexing, Printing (20:31)
    71. Part D: Version 2 - 2D Array Extended with Error Checking (32:28)
  • Week 11: Two-Dimensional Arrays (Part II: Utility Methods)
    72. Part A1: Example 1: Displaying Elements Row by Row (21:31)
    73. Part A2: Example 1: Displaying Elements Column by Column (16:04)
    74. Part B: Example 2: Overall Average vs. Row Averages (27:47)
    75. Part C: Example 3: Returning Max/Min Values (with Exercise) (16:02)
    76. Part D: Example 4: Returning the Row with Maximum Sum (17:47)
    77. Part E: Example 5: Checking the All-Positive Universal Property (with Exercise) (22:03)
    78. Part F: Example 6: Rectangular Shape? (with Exercise) (17:38)
    79. Part G: Example 7: Displaying Lower-Left vs. Upper-Left Triangular Areas (13:38)
  • Week 12: Java API Case Studies: Building a Birthday Book Application
    80. Part A: Problem - Birthday Book Application (14:21)
    81. Part B: BirthdayBook - Method Headers and JUnit Tests (26:39)
    82. Part C1: BirthdayBook Implementation V1 using ArrayList - Coding (32:03)
    83. Part C2: BirthdayBook Implementation V1 using ArrayList - Tracing (28:37)
    84. Part D1: BirthdayBook Implementation V2 using Hashtable - Coding (17:35)
    85. Part D2: BirthdayBook Implementation V2 using Hashtable - Tracing (21:34)

•  Java from Scratch: from Procedural to Object-Oriented Programming ( iPad Notes)

  This tutorial series assumes no knowledge of Java and the working environment is Eclipse.

  • Simple Console Applications using Primitive Variable Assignments
    1. Class, main method, print statement, sequential execution (27:26)
    2. Basic numerical literals and operations (25:16)
    3. String literals, concatenating strings and numbers (33:23)
    4. Literals vs. variable, declaring/initializing/re-assigning variables (32:05)
    5. Swapping values of two variables (33:06)
    6. Customizing Java perspective in Eclipse (10:11)
    7. Console Application: Prompt, Read, Process, Output (47:57)
    8. Synchronizing Java projects between personal and lab computers (9:49)
  • Simple If-Statements using the Boolean Data Type and Logical Operations
    9. Closing the latest Github repository, creating a lab Java project (4:09)
    10. Boolean data type and literals, relational operations (26:37)
    11. Logical operations, truth table (33:21)
    12. Negation, double negation (21:34)
    13. Conjunction for including integer interval, false by disjunction (27:09)
    14. Disjunction for excluding integer interval, false by conjunction (32:21)
    15. If-statement: calculating absolute value (15:59)
    16. If-statement: calculating account withdrawal (if-else) (32:31)
    17. If-statement: calculating account withdrawal (if-elseif-else) (27:47)
  • A Simple Bank Account Application using Nested If-Statements
    18. A simple bank application (nested if-statements Version 1) (1:03:08)
    19. A simple bank application (nested if-statements Version 2) (1:03:41)
  • Syntax and Semantics of for-Loops and while-Loops, Using Breakpoints and Debugger in the Programming IDE to Reveal Defects
    20. Break points and debugger (swap program, nested if-statements) (52:28)
    21. Introduction to for-loops, flow chart, tracing (27:34)
    22. Console application using for-loops, tracing (23:33)
    23. Introduction to while-loops, flow chart, tracing (18:57)
    24. Console application with error handling using while-loops, tracing (43:51)
  • Basics of Arrays: Initialization using Loops and Tracing
    25. Array initializer, indexing, iteration, exception on bounds (56:45)
    26. Creating a fix-sized array, re-assigning array and elements, tracing (43:00)
    27. Initialing array using a loop, tracing (55:07)
    28. Creating an array with user-input size, tracing (22:32)
  • Deciding if Array Elements Universally/Existentially Satisfy Given Properties
    29. All numbers positive? (V1: entire array with accumulation) (44:49)
    30. Some number positive? (V1: entire array with accumulation) (36:01)
    31. All/Some positive? (V2: entire array without accumulation) (26:18)
    32. All/Some positive? (V3/V4: early exit with/out accumulation) (1:02:18)
    33. Array sorted? (V4: early exit without accumulation) (25:31)
  • Object Orientation: Classes, Methods, Object Creations, and Method Calls
    34. Classes, attributes, constructors, visualizing object creations (1:04:02)
    35. Visualizing object creations using overloaded constructors (41:39)
    36. Use of this keyword in constructors (30:58)
    37. Defining and calling accessor methods, context objects (1:00:03)
    38. Defining and calling mutator methods, context objects (28:25)
    39. Format, expectation, workflows for OO labs and lab test (20:34)
  • Understanding and Implementing Associations between Classes
    40. Faculty class, console tester, aliasing (1:07:20)
    41. CourseRecrod class, reference-typed attribute, aliasing (1:23:56)
    42. Student class, array-typed attribute, aliasing, null reference (1:18:07)
    43. Inter-connected objects with aliasing (44:26)
    44. Alternative version of the addCoruse mutator method (30:21)
    45. Defining and using helper methods (44:06)
    46. Adding accessor methods to CourseRecord and Student classes (28:56)

  Back to Roadmap

  ---

•  Developing an Apple Refurbished Store App ( iPad Notes)
  • Part 1: Single Class with Primitive-Typed Attributes
    0. Study Resources (12:03)
    1. Separation of Concerns, Eclipse Work Environment (20:03)
    2. Object Orientation (observe-model-execute), Motivating Problem - Apple Refurbished Store (18:28)
    3. Product Class: Attributes and Implicit, Default Constructor (14:02)
    4. Product Class: Debugger, Default Values, Printing Addresses, and Explicit, Default Constructor (18:38)
    5. Product Class: Overloaded Constructor, Console Application with a Scanner (18:47)
    6. Product Class: Tracing Object Creations on Debugger and Paper (20:20)
    7. Product Class: Generating Getters and Setters (15:14)
    8. Product Class: Accessors getPrice() and toString() (18:58)
    9. TestProduct Class: Testing Default Constructor - String and int Return Values (18:43)
    10. TestProduct Class: Testing Default Constructor - boolean and double Return values (14:39)
    11. TestProduct Class: Testing Overloaded Constructor, assertTrue(stringValue1 == stringValue2) (18:37)
    12. TestProduct Class: Testing Mutator Method Calls (16:15)
    13. TestProduct Class: Tracing Object Creation and Method Calls (29:35)
  • Part 2: Inter-Associated Classes with Reference-Typed Attributes
    14. Entry Class: Single-Valued, Reference-Typed Attribute (14:08)
    15. Entry Class: Mutator setProduct and toString method (reusing toString from Product) (16:28)
    16. TestEntry Class: assertSame on object addresses (16:18)
    17. TestEntry Class: toString method from Product vs. Entry (19:02)
    18. TestEntry Class: Changing the Reference of an Entry's Product (22:31)
    19. TestEntry Class: Idea of Reference Aliasing (09:42)
    20. TestEntry Class: Tracing of Reference Aliasing (44:16)
    21. RefurbishedStore Class: Multi-Valued, Reference-Typed Attributes (17:12)
    22. RefurbishedStore Class: Adding and Retrieving Entries (18:57)
    23. TestRefurbishedStore Class: Adding Multiple Entries (26:38)
    24. TestRefurbishedStore Class: Tracing How Entries Are Added (debugger) (09:39)
    25. TestRefurbishedStore Class: Tracing How Entries Are Added (paper) (33:39)
    26. RefurbishedStore Class: Modifying the Same Object via Different Aliases (22:56)
    27. RefurbishedStore Class: Tracing the NullPointerException in the Debugger (11:33)
    28. RefurbishedStore Class: getSpaceGreyOrPro - Visual Sketch (15:56)
    29. RefurbishedStore Class: getSpaceGreyOrPro - Implementation (10:17)
    30. RefurbishedStore Class: getSpaceGreyOrPro - Unit Testing and Debugging (16:36)

  Back to Roadmap

  ---

•  Developing a Birthday Book App (Problem ;  iPad Notes)
  • Part 00 - Problem and Setup
  • Part 01 - Birthday class, attributes, constructor, and accessors
  • Part 02 - Birthday class, toString method, Precondition for constructor
  • Part 03 - Birthday class, equals method
  • Part 04 - Entry class, attributes, constructor (version 1), accessors, toString method
  • Part 05 - Entry class, constructor (version 2)
  • Part 06 - Entry class, equals method
  • Part 07 - Entry class, setName and setBirthday, default setBirthday generated by Eclipse vs. customized setBirthday
  • Part 08 - Entry class, default setBirthday generated by Eclipse vs. customized setBirthday
  • Part 09 - BirthdayBook class, constructor, attribute Entry[] entries, attribute int noe, method int getNumberOfEntries, method Entry[] getEntries()
  • Part 10 - BirthdayBook class, toString method (case of empty book)
  • Part 11 - BirthdayBook class, nameExists method (case of empty book), private helper method indexOf(name)
  • Part 12 - BirthdayBook class, getBirthday method (case of empty book), private helper method indexOf(name)
  • Part 13 - BirthdayBook class, getReminders(Birthday) method, getReminders(int m, int d) method
  • Part 14 - BirthdayBook class, removeEntry (case of empty book), common mistake of getEntries
  • Part 15 - BirthdayBook class, addEntry(name, birthday) vs. addEntry (name, month, day)
  • Part 16 - BirthdayBook class, toString method (non-empty book)
  • Parts 17 to 21 - BirthdayBook class, assertions on nameExists, getBirthday, getReminders
  • Parts 22 to 23 - BirthdayBook class, removeEntry (case of non-empty book), Illustrations on the algorithm
  • Parts 24 to 27 - BirthdayBook class, No new development, Converting console interactions to JUnit test method
  • Parts 28 to 30 - BirthdayBook class, addEntry (case of existing name)
  • Parts 31 to 35 - BirthdayBook class, equals method

  Back to Roadmap

  ---

•  Java Collections ( iPad Notes)
  • Part 1: ArrayList
  • Part 2: HashMap

Back to Roadmap

Eclipse

• Importing a Project from an Archive File
• Setting VM Argument for Assertions

  Back to Roadmap

Objected Oriented Programming in Android Studio

•  Developing a BMI Calculator App (Problem ;  iPad Notes)

  App Development Pattern: Single Button Manipulating a Single Model Object

  • Setup (Start from here if you are using your own computer)
    • Part 00 - Download VirtualBox Tool and Image
    • Part 01 - Setup a Shared Folder between the Host and Virtual Machines
  • Setup (Start from here if you are using a lab machine)
    • Part 02 - Launch Android Studio from the Virtual Machine
    • Part 03 - Create a New Project, Explore the Project Structure
    • Part 04 - Change the Editor Font Face and Size for the Android Project
  • View (as in the Model-View-Controller Pattern)
    • Part 05 - Design of View (as in Mode-View-Controller)
    • Part 06 - Program the GUI Design of View in Android Studio
    • Part 07 - Anatomy of the .xml File for the View
    • Part 08 - Run the app as is with Only the View Implemented
  • Controller (as in the Model-View-Controller Pattern)
    • Part 09 - Attach a Method from Controller to some GUI Component
    • Part 10 - Call Helper Methods in Controller to Retrieve User Entered Inputs, Re-Launch the app
    • Part 11 - Convert Retrieved Inputs to Numbers, Compute the BMI in Controller, and Re-Launch the app
    • Part 12 - Doing the app-Specific Computation in Controller Violates the Separation of Concern Principle
  • Model (as in the Model-View-Controller Pattern)
    • Part 13 - Create a Tester (with a main method) for Test Driven Development (TDD)
    • Part 14 - Object Orientation (entities, classes, attributes, behaviour)
    • Part 15 - Declare a Person class, Declare Person's Attributes, and Crate a Tester for the Person class
    • Part 16 - Define, Test, and Debug the Person Constructor
    • Part 17 - Define, Test, and Debug the getBMI and toString Accessor Methods
    • Part 18 - Define, Test, and Debug the setWeight(double w) Mutator Method
    • Part 19 - Add Code that Manipulates Model Person Objects in the Controller, and Re Launch the app
  • Conclusion
    • Part 20 - Summary: Model-View-Controller (MVC) Pattern, Object Orientation (OO), and Test-Driven Development (TDD)

  Back to Roadmap

  ---

•  Developing a Counter App ( iPad Notes)

  App Development Pattern: Multiple Buttons Sharing a Single Model Object

  • Part 1 - Setting Up the Project
  • Part 2 - GUI Design for the View
  • Part 3 - Attaching Controller Methods to GUI Buttons
  • Part 4 - Defining a Counter Model using Test-Driven Development (TDD) and Debugger
  • Part 5 - Connecting the Controller and Model (Multiple-Objects vs. Single-Shared-Object)

  Back to Roadmap

  ---

•  Developing Point and PointeCollector Model Classes ( iPad Notes)

  Model Development Pattern: Declaring Attributes with Reference Types

  • Part 1 - Assignments of Reference Variables, Aliasing
  • Part 2 - Attributes with Reference Types, Mutator Methods that Modify Reference Typed Attributes

  Back to Roadmap

  ---

•  Developing CourseRecord, Student, and StudentManagementSystem Model Classes ( iPad Notes)

  Model Development Pattern: Declaring Attributes with Array-Referenced Types

  • Part 00 Creating a No-Activity Project
  • Part 01 Defining/Testing the CourseRecord Class
  • Part 02 Student Class - Maintaining an Array of CourseRecord Objects
  • Part 03 Student Class - Demystifying the Dot Notation
  • Part 04 Student Class - Alternative Mutator for Adding a CourseRecord
  • Part 05 Student Class - Aliasing of CourseRecord Objects
  • Part 06 Student Class - Accessor getMarks and Mutator setMarks
  • Part 07 Student Class - Refactoring getMarks and setMarks using indexOfCourse
  • Part 08 Student Class - Defining Accessor Method getGPA using Helper Method getGP
  • Part 09 Student Class - Adding Error Handing via New Attributes error and errorMsg
  • Part 10 StudentManagementSystem Class - Maintaining an Array of Student Objects
  • Part 11 StudentManagementSystem Class - Revisiting the Dot Notation and Aliasing
  • Part 12 StudentManagementSystem Class - Adding a CourseRecord at the SMS Level
  • Part 13 StudentManagementSystem Class - Getting and Setting Marks at the SMS Level
  • Part 14 StudentManagementSystem Class - Getting the GPA at the SMS Level
  • Part 15 StudentManagementSystem Class - Error Handing via Attributes error and errorMsg

Back to Roadmap

---

Software Design

•  Introductory Tutorial: Eiffel Language/Method/Tool for Design (Fall 2020)

  Study Notes:

  •  iPad Notes
  • Each section in this document summarizes main points of the corresponding tutorial video.
  1. Unit Testing & Console Outputting, Run vs. Run Workbench System (28:57)
  2. Setting Tools Layout, Navigating Library Classes (20:10)
  3. BIRTHDAY: Variable Declarations, Features, Invariant (20:43)
  4. BIRTHDAY: Static Queries, TDD, Boolean Test Case (28:09)
  5. BIRTHDAY: Assertions, Logical Operator Precedence (25:48)
  6. BIRTHDAY: Syntax Overview of Classes and Features (08:40)
  7. BIRTHDAY: Using a Command as a Constructor (24:06)
  8. BIRTHDAY: Setting Breaking Points and Launching Debugger (15:16)
  9. BIRTHDAY: Writing a Precondition Violation Test (34:45)
  10. BIRTHDAY: Writing a Postcondition Test (30:13)
  11. BIRTHDAY: Reference Equality vs. Object Equality (21:20)
  12. BIRTHDAY: Logical Pattern for Invariant (09:35)
  13. Basic Operations of Arrays (30:58)
  14. Basic Operations of Linked Lists (17:01)
  15. Use of across as Loop Instructions (23:46)
  16. Use of across as Boolean Expressions (21:28)
  17. BIRTHDAY_BOOK: Attributes, Constructor, Void Safety (27:32)
  18. BIRTHDAY_BOOK: Class Invariant (16:46)
  19. BIRTHDAY_BOOK: Command add - Debugging Precondition (30:45)
  20. BIRTHDAY_BOOK: Command add - Testing Postcondition (35:16)
  21. BIRTHDAY_BOOK: Get Birthday -- detachable? [Supplier] (39:52)
  22. BIRTHDAY_BOOK: Get Birthday -- detachable? [Client] (24:49)
  23. BIRTHDAY_BOOK: Exercise -- Implement and Specify Query celebrate (18:57)

  Back to Roadmap

  ---

•  Use of Eiffel Studio for DbC and TDD (Summer 2015)

  NOTES: Follow each tutorial video with its associated section in this document, which also contains links to the corresponding tutorial videos.

  1. Create a New Project and Set Clusters
  2. Add the ACCOUNT Class
  3. Add a Class for Testing ACCOUNT
  4. How a Test Case Fails
  5. Use Breakpoints and Debugger
  6. Specify Contracts for Withdraw
  7. Add Transaction and Date into Context
  8. Uniform Access of Account Balance

  Back to Roadmap

  ---

•  Generic Parameters and the Iterator Pattern

  1. A Book of Any vs. A Generic Book

     Follow this tutorial video with this document.

  2. Making the Generic Book Iterable

     Follow this tutorial video with Section 3 of this lab session.

  Back to Roadmap

  ---

•  Information Hiding and the Iterator Pattern

  1. Information Hiding -- An Online Shopping System

     Follow this tutorial video with this document.

  2. Making the Cart of Orders Iterable

     Follow this tutorial video with Section 2 of this lab session.

  Back to Roadmap

  ---

•  Eiffel Testing Framework (ETF): a Framework for Testing Design

  Written ETF Tutorial: A Simple Banking System

  Script for Regression Testing of Acceptance

  Oracle Program (Linux executable) for the Bank Example

  0. (Optional) Setting Environment Variable for the MATHMODELS library on your home machine
  1. Using a text file specifying the abstract user interface (of a bank system) to generate a starter ETF project.
  2. Launching the starter project in the default GUI mode and changing to command-line (interactive or batch) mode, and developing acceptance tests.
  3. Architecture of classes in cluster user_commands and cluster model, making changes, and re-running acceptance tests.
  4. Developing Model Classes and re-running acceptance tests.
  5. DbC in model classes, error reporting in command classes, and debugging in EStudio
  6. Acceptance Tests, Expected Outputs, Actual Outputs
  7. Automating Regression Testing (from home to school computers)

  Back to Roadmap

  ---

•  Design Patterns: Composite and Visitor

  1. Setting up the Project
  2. Implementing the Composite Pattern
  3. Debugging the Composite Pattern
  4. Implementing the Visitor Pattern
  5. Debugging the Visitor Pattern
  6. Open Closed Principle on the Visitor Pattern

  Back to Roadmap

Formal Methods for System Development

•  Introduction to the Rodin Platform for Formal Specifications ( iPad Notes)

  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.

  • Part A - Launching Rodin from EECS Remote Lab, New Project (11:31)
  • Part B - Configuring Post-Tactics of an Event-B Project (08:14)
  • Part C - Requirements Document of a Bank System (17:07)
  • Part D1 - Specifying Context: Constants and Constraints (14:55)
  • Part D2 - Specifying Context: Axioms vs. Theorems (14:18)
  • Part E1 - Specifying Machine: Modelling Decision on Variable (15:13)
  • Part E2 - Typing Constraint as Invariant, INITIALIZATION (09:49)
  • Part E3 - Using a Wizard, Specifying Update as Overriding (19:41)
  • Part E4 - Specifying an Event: Parameters, Guards, Actions (08:14)
  • Part E5 - Understanding and Fixing Well-Definedness (WD) (12:34)
  • Part F - Exercise: Undersand and Fix Failed withdraw/inv3 (18:31)

  Back to Roadmap

  ---

•  Introduction to the TLA+ Toolbox for Formal Specifications ( iPad Notes)

  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.

  • Part A - Launching TLA+ from EECS Remote Lab, Background (14:17)
  • Part B - Revisiting the Bridge Controller (25:37)
  • Part C1 - Context: Import, Constants, Axioms (24:35)
  • Part C2 - Algorithm: Variables, Assignments, Choices, Loops, Procedures (26:13)
  • Part C3 - Bounded Interleaving of Events (13:26)
  • Part D1 - Translating PlusCal Algorithm to TLA+ (17:20)
  • Part D2 - Adding Labels for More Informative Generated TLA+ (12:50)
  • Part D3 - Understanding Generated TLA+ Predicates (31:07)
  • Part E1 - Invariants and Deadlock Freedom, Setting for State Graph (30:21)
  • Part E2 - Debugging Models via Error Trace and State Graph, Exercises (29:39)

  Back to Roadmap