A formally specified tournament management web app. The system logic was first defined using VDM-SL (a formal specification language), then implemented as a single-page web application with HTML, CSS, and vanilla JavaScript.
The idea was to make sure every feature in the app has a mathematically precise definition — every operation has pre-conditions that must be true before it runs, and post-conditions that confirm the state changed correctly.
Tournament organizers can run a full competitive tournament from start to finish through a dashboard with six sections:
- Players — register players with unique IDs, track wins and losses, remove unassigned players
- Teams — create teams, add/remove players from rosters, disqualify teams
- Matches — schedule matches between two active teams, start them, record results, or cancel
- Bracket — generate the tournament bracket once teams are ready; winners advance through rounds
- Prizes — add trophies, cash prizes, or medals to the pool; assign to the winner once the tournament ends
- Dashboard — live stats showing total players, active teams, scheduled matches, and total prize pool
Every action is validated against the formal spec rules before it executes. If a pre-condition fails, the operation is rejected with an error message and nothing changes.
| File | What it is |
|---|---|
GameTournament.vdmsl |
Formal specification in VDM-SL — the mathematical definition of every operation, type, and invariant |
app.js |
JavaScript implementation — the same logic, built into a working web app |
index.html |
Single-page dashboard UI |
styles.css |
Dark glassmorphic design |
- A player can only belong to one team at a time
- A team needs at least 2 members before it can play a match
- Matches can only be scheduled after the bracket is generated
- Recording a result automatically eliminates the losing team
- Prizes can only be assigned when exactly one active team remains
- Once the tournament starts, team rosters are locked
The formal specification covers 5 modules with 17 operations total:
- Player Management — RegisterPlayer, RemovePlayer, GetPlayerStats
- Team Management — CreateTeam, AddPlayerToTeam, RemovePlayerFromTeam, DisqualifyTeam
- Match Management — ScheduleMatch, StartMatch, RecordResult, CancelMatch, GetMatchHistory
- Bracket Management — GenerateBracket, AdvanceWinner, GetCurrentRound
- Prize Management — AddPrize, AssignPrizeToWinner, GetPrizeList
├── index.html # single-page dashboard
├── styles.css # dark theme, glassmorphic design
├── app.js # all tournament logic and UI rendering
├── GameTournament.vdmsl # formal VDM-SL specification
└── README.md
No installation needed. Just open index.html in a browser. All logic runs client-side — no backend, no database. Note that state is in-memory and resets on page refresh.
To open and validate the VDM-SL spec, use the Overture IDE.
- HTML5, CSS3, Vanilla JavaScript (ES6+)
- VDM-SL for formal specification (Overture IDE)
Mohamed Tariq, Ahmed Deaiy, Freddy George, Mostafa Mohsen, Mohanned Elsawy