Contents Collection of Lists Modelling a list of items Queues Modelling a Printer Queue Relating jobs and queue positions Ass...
Lists and Collections in Event-B
Proof-Based Verification in Event-B
Contents Validation and Verification Validation Verification What is Formal Verification? Proof Obligations (PO) ...
For ISP, What Is an "Interface"?
The key to understanding the principle of interface separation is to understand the word “interface”. In fact, the term “interface” can be used in many contexts. In software development, we can ei...
For OCP, What Exactly Are "Extensions" and "Modifications"?
The Open/Closed Principle (OCP) is a cornerstone in crafting maintainable, scalable, and robust OOP systems. It encourages us to think ahead, design with flexibility in mind, and respect the existi...
For SRP, How Do We Determine If a Class Has a "Single" Responsibility?
Many people think that SRP is the simplest principle in SOLID because they think that it is very easy to give modules a single responsibility. Actually, it’s not. In my opinion, SRP is the hardest ...
SOLID Principles
Design principles and ideas are more universal and important than design patterns. Contents What are SOLID principles? Single Responsibility Principle (SRP) Concept ...
Extension Refinement in Event-B
Contents What is Refinement? Extension Example: add ownership to secure database Original Example Adding Object Ownership in the Original Example What is ...
Hoare Logic
Contents Foreword Logic Completely Convincing Arguments: Logical Fallacy Completely Convincing Arguments: Sound Inferences What is Hoare Logic? ...
Bounded Model Checking
Contents What is Bounded Model Checking? Why bounded? Model Checking versus Bounded Model Checking Bounded Model Checking for Reachability Example: Two Bit Cou...
Clean Code: Unit Tests
Unit tests are a fundamental part of writing clean, maintainable, and robust code. They guide the design, provide documentation, and safeguard against future changes or refactoring. By adhering to ...