Skip to content

A short single-file program detailing a newspaper delivery route using B-Method and formal specification!

Notifications You must be signed in to change notification settings

Cselwood/PaperRoundBMachine

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

5 Commits
 
 
 
 

Repository files navigation

PaperRoundBMachine

B-Method newspaper delivery system!

Using B-Method and Formal Specification, this delivery route system is programmed to be safety-critical, and defect-free using the B-Method on AtelierB and animated in ProB software. The program details names of different available newspapers and magazines in the United Kingdom, and houses on the road that require each item. It ensures the program is bug-free by using B-Method and stating explicitly the relationships between newspapers, magazines and houses that want (or don't) those items. This program was originally designed by me at University.

Features

- Has a wide array of reading items available
- Ensures each house only gets delivered what it has ordered
- Is guaranteed to be bug free by being developed in an abstract machine

How It's Made!

- Entirely in B-Method
- Using set theory, and relationships
- Designed as a standlone abstract machine!

Installation

Clone the file and upload to your own ProB software, alternatively any software which can edit B (such as AtelierB) can be used to edit and improve the code.

Release History

  • 1.0
    • Full public release

Meta

Distributed under the MIT license. See LICENSE for more information.

https://github.com/Cselwood

Contributing

If you see an issue, an efficiency that could be made, or an improvement, program away! Fork it if you like (https://github.com/Cselwood/PaperRoundBMachine/fork)

About

A short single-file program detailing a newspaper delivery route using B-Method and formal specification!

Topics

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published