Advanced course
Techniques for modelling real legal systems in L4. It assumes you have completed the Foundation course or already write L4.
The course covers real regulatory schemes, patterns that cut across many rules (timing, notices, appeals), contracts in depth, and how to structure, test and deploy a real rulebase. Take the modules in order.
Modules
- Module A1: Real regulatory schemes: the three-layer approach, definitions and cross-references, built on a charity regulation example.
- Module A2: Cross-cutting concerns: deadlines, notice and cure, appeals, escalation and grace periods.
- Module A3: Contracts in depth: payment terms, recursive obligations and penalties, built on a promissory note.
- Module A4: Production patterns: structuring a real rulebase into files and sections, testing it, and getting it ready to deploy.
Example code
Modules A1 to A3 each come with a complete, validated example file:
-- Module A1: Real Regulatory Schemes - Complete Example
-- Charity Registration System based on Jersey Charities Law 2014
--
-- This file demonstrates the three-layer approach to encoding legislation:
-- Layer A: Structural Definitions (types from statutory glossary)
-- Layer B: Deontic Rules (obligations, permissions, prohibitions)
-- Layer C: Events and State Transitions
IMPORT prelude
IMPORT daydate
-- ============================================================
§ `Layer A: Structural Definitions`
-- ============================================================
-- Supporting types needed by the main definitions
DECLARE Conviction HAS
`the offence` IS A STRING
`the date` IS A DATE
`involves dishonesty` IS A BOOLEAN
DECLARE Money HAS
`the amount` IS A NUMBER
`the currency` IS A STRING
DECLARE Asset HAS
`the description` IS A STRING
`the value` IS A Money
DECLARE Applicant HAS
`the name` IS A STRING
`the contact` IS A STRING
-- Article 2(10): "misconduct" includes mismanagement or misapplication
DECLARE `Misconduct Type` IS ONE OF
Mismanagement
Misapplication
`other misconduct` HAS `the description` IS A STRING
-- Schedule 1: Charitable purposes (13 statutory heads)
DECLARE `Charitable Purpose` IS ONE OF
`prevention or relief of poverty`
`advancement of education`
`advancement of religion`
`advancement of health or saving of lives`
`advancement of citizenship or community development`
`advancement of arts, culture, heritage or science`
`advancement of amateur sport`
`advancement of human rights, conflict resolution, reconciliation`
`advancement of environmental protection or improvement`
`relief of those in need`
`advancement of animal welfare`
`purposes analogous to charitable purposes`
`other charitable purpose` HAS `the description` IS A STRING
-- Article 2: Governor definition
DECLARE Governor HAS
`the name` IS A STRING
`the date of birth` IS A DATE
`the address` IS A STRING
`is bankrupt` IS A BOOLEAN
`the convictions` IS A LIST OF Conviction
-- Core financial information (Regulation 1, Core Info Regs 2018)
DECLARE `Core Financial Information` HAS
`the income` IS A Money
`the expenditure` IS A Money
`the opening assets` IS A Money
`the closing assets` IS A Money
`the other assets` IS A LIST OF Asset
-- Register sections
DECLARE `Register Section` IS ONE OF
`the general section`
`the restricted section`
-- Charity status
DECLARE `Charity Status` IS ONE OF
Pending
Active
Suspended HAS
`the reason` IS A STRING
`the date` IS A DATE
Deregistered HAS
`the reason` IS A STRING
`the date` IS A DATE
`is retrospective` IS A BOOLEAN
-- Main charity record
DECLARE `Registered Charity` HAS
`the name` IS A STRING
`the registration number` IS A STRING
`the register section` IS A `Register Section`
`the status` IS A `Charity Status`
`the constitution` IS A STRING
`the purposes` IS A LIST OF `Charitable Purpose`
`the public benefit statement` IS A STRING
`the governors` IS A LIST OF Governor
`the financials` IS A `Core Financial Information`
`the registration date` IS A DATE
-- Reportable matters under Article 19(1)
DECLARE `Reportable Matter` IS ONE OF
Bankruptcy HAS
`the date` IS A DATE
`director disqualification` HAS
`the date` IS A DATE
`the jurisdiction` IS A STRING
`dishonest conviction` HAS
`the description` IS A STRING
`the date` IS A DATE
-- ============================================================
§ `Layer B: Deontic Definitions`
-- ============================================================
-- Actors in the regulatory system
DECLARE Actor IS ONE OF
`the charity` HAS `the charity record` IS A `Registered Charity`
`the governor` HAS `the governor record` IS A Governor
`the Commissioner`
`the applicant` HAS `the applicant record` IS A Applicant
-- Actions that can be performed
DECLARE Action IS ONE OF
-- Charity obligations
`file annual return`
`report change of particulars`
`report reportable matter` HAS
`the matter` IS A `Reportable Matter`
-- Commissioner powers
`demand information`
`issue Required Steps Notice`
`suspend governor` HAS
`the reason` IS A STRING
`deregister charity` HAS
`the reason` IS A STRING
-- Governor obligations
`act in best interests`
`report conviction`
-- Appeal actions
`lodge appeal`
-- ============================================================
§ `Layer B: Deontic Rules`
-- ============================================================
-- B-AR-01: Annual Return Obligation
-- Article 13(7)-(10) + Timing Order 2019
-- "A registered charity must file an annual return within 2 months of year end"
GIVEN charity IS A `Registered Charity`
GIVETH A DEONTIC Actor Action
`annual return obligation` MEANS
IF charity's `the status` EQUALS Active
THEN
PARTY `the charity` charity
MUST `file annual return`
WITHIN 60 -- 2 months approximately 60 days
HENCE FULFILLED
LEST `Commissioner may issue notice` charity
ELSE FULFILLED
-- B-RSN-01: Commissioner's Power to Issue Notice
-- Article 27(1)-(4)
GIVEN charity IS A `Registered Charity`
GIVETH A DEONTIC Actor Action
`Commissioner may issue notice` MEANS
PARTY `the Commissioner`
MAY `issue Required Steps Notice`
HENCE `charity must comply with notice` charity
-- B-RSN-02: Charity must comply with notice
-- Article 27(5)
GIVEN charity IS A `Registered Charity`
GIVETH A DEONTIC Actor Action
`charity must comply with notice` MEANS
PARTY `the charity` charity
MUST `file annual return`
WITHIN 30
HENCE FULFILLED
LEST BREACH BY `the charity` charity BECAUSE "Failed to comply with Required Steps Notice"
-- B-GOV-02: Governor reporting obligation
-- Article 19(1): A governor must notify the Commissioner as soon as practicable
-- if any reportable matter applies to them
GIVEN governor IS A Governor
matter IS A `Reportable Matter`
GIVETH A DEONTIC Actor Action
`governor reporting obligation` MEANS
PARTY `the governor` governor
MUST `report reportable matter` matter
WITHIN 14 -- "as soon as practicable" interpreted as 14 days
HENCE FULFILLED
LEST `Commissioner may suspend` governor
-- B-GOV-03: Commissioner may suspend governor
-- Article 29
GIVEN governor IS A Governor
GIVETH A DEONTIC Actor Action
`Commissioner may suspend` MEANS
PARTY `the Commissioner`
MAY `suspend governor` "Failed to report reportable matter"
HENCE FULFILLED
-- ============================================================
§ `Layer C: Events and State Transitions`
-- ============================================================
-- Events that change the register
DECLARE `Register Event` IS ONE OF
`charity registered` HAS
`the charity record` IS A `Registered Charity`
`the date` IS A DATE
`charity moved to restricted` HAS
`the charity record` IS A `Registered Charity`
`the date` IS A DATE
`charity deregistered` HAS
`the charity record` IS A `Registered Charity`
`the reason` IS A STRING
`the date` IS A DATE
`is retrospective` IS A BOOLEAN
`annual return filed` HAS
`the charity record` IS A `Registered Charity`
`the year` IS A NUMBER
`was late` IS A BOOLEAN
`Required Steps Notice issued` HAS
`the charity record` IS A `Registered Charity`
`the notice id` IS A STRING
`the deadline` IS A DATE
`governor suspended` HAS
`the governor record` IS A Governor
`the charity record` IS A `Registered Charity`
`the reason` IS A STRING
`the period` IS A NUMBER
-- Effect of events on register
GIVEN event IS A `Register Event`
GIVETH A STRING -- Describes the effect
`event effect` MEANS
CONSIDER event
WHEN `charity registered` c d THEN
"New active entry created in register"
WHEN `charity deregistered` c r d retro THEN
IF retro
THEN "Entry moved to historic; registration void from earlier date"
ELSE "Entry moved to historic"
WHEN `annual return filed` c y late THEN
IF late
THEN "Annual return logged with late flag"
ELSE "Annual return logged"
WHEN `Required Steps Notice issued` c nid deadline THEN
"Notice reference stored under Art 8(3)(k)"
OTHERWISE "Register updated"
-- ============================================================
§ `Cross-References and Charity Test`
-- ============================================================
-- The charity test (Article 5) references:
-- - Schedule 1 (purposes)
-- - Article 7 (public benefit)
-- - Regulations (core financial info)
GIVEN charity IS A `Registered Charity`
GIVETH A BOOLEAN
DECIDE `meets charity test` IF
`has charitable purposes` charity -- Schedule 1
AND `provides public benefit` charity -- Article 7
AND `has valid constitution` charity -- Article 11(2)(a)
AND `has complete financial info` charity -- Core Info Regs
-- Stub: Check if charity has at least one charitable purpose
GIVEN charity IS A `Registered Charity`
GIVETH A BOOLEAN
DECIDE `has charitable purposes` IF
NOT (null (charity's `the purposes`))
-- Article 7: Public benefit factors
GIVEN charity IS A `Registered Charity`
GIVETH A BOOLEAN
DECIDE `provides public benefit` IF
`has identifiable benefit` charity -- Art 7(2)(a)
AND `benefit outweighs detriment` charity -- Art 7(2)(b)
AND NOT `unduly restricts beneficiaries` charity -- Art 7(3)
-- Stub implementations for public benefit factors
GIVEN charity IS A `Registered Charity`
GIVETH A BOOLEAN
DECIDE `has identifiable benefit` IF
NOT (charity's `the public benefit statement` EQUALS "")
GIVEN charity IS A `Registered Charity`
GIVETH A BOOLEAN
DECIDE `benefit outweighs detriment` IF
TRUE -- Would need detailed analysis
GIVEN charity IS A `Registered Charity`
GIVETH A BOOLEAN
DECIDE `unduly restricts beneficiaries` IF
FALSE -- Would need detailed analysis
GIVEN charity IS A `Registered Charity`
GIVETH A BOOLEAN
DECIDE `has valid constitution` IF
NOT (charity's `the constitution` EQUALS "")
GIVEN charity IS A `Registered Charity`
GIVETH A BOOLEAN
DECIDE `has complete financial info` IF
charity's `the financials`'s `the income`'s `the amount` >= 0
AND charity's `the financials`'s `the expenditure`'s `the amount` >= 0
-- ============================================================
§ `Handling Amendments - Temporal Validity`
-- ============================================================
-- Original Law 2014 had 12 charitable purposes
-- R&O 27/2025 added "advancement of animal welfare"
-- Model with effective dates:
DECLARE `Dated Purpose` HAS
`the purpose` IS A `Charitable Purpose`
`effective from` IS A DATE
-- Check if purpose was valid at a given date
GIVEN purpose IS A `Charitable Purpose`
`the reference date` IS A DATE
GIVETH A BOOLEAN
DECIDE `purpose valid at date` IF
-- Animal welfare only valid from 2025
IF purpose EQUALS `advancement of animal welfare`
THEN `the reference date` >= Date 1 1 2025
ELSE TRUE -- Other purposes valid from 2014
-- ============================================================
§ `Test Data`
-- ============================================================
-- Sample governor
`John Smith` MEANS Governor WITH
`the name` IS "John Smith"
`the date of birth` IS Date 15 6 1975
`the address` IS "123 Main Street, St Helier"
`is bankrupt` IS FALSE
`the convictions` IS EMPTY
-- Sample financial info
`sample financials` MEANS `Core Financial Information` WITH
`the income` IS Money WITH `the amount` IS 50000, `the currency` IS "GBP"
`the expenditure` IS Money WITH `the amount` IS 45000, `the currency` IS "GBP"
`the opening assets` IS Money WITH `the amount` IS 100000, `the currency` IS "GBP"
`the closing assets` IS Money WITH `the amount` IS 105000, `the currency` IS "GBP"
`the other assets` IS EMPTY
-- Sample active charity
`Acme Animal Shelter` MEANS `Registered Charity` WITH
`the name` IS "Acme Animal Shelter"
`the registration number` IS "JC-2024-001"
`the register section` IS `the general section`
`the status` IS Active
`the constitution` IS "Standard charitable constitution"
`the purposes` IS LIST `advancement of animal welfare`
`the public benefit statement` IS "Provides shelter and care for abandoned animals in Jersey"
`the governors` IS LIST `John Smith`
`the financials` IS `sample financials`
`the registration date` IS Date 15 1 2024
-- ============================================================
§ `Test Traces`
-- ============================================================
-- Test 1: Active charity files annual return on time
#TRACE `annual return obligation` `Acme Animal Shelter` AT 0 WITH
PARTY `the charity` `Acme Animal Shelter` DOES `file annual return` AT 30
-- Test 2: Active charity misses deadline, commissioner issues notice
#TRACE `annual return obligation` `Acme Animal Shelter` AT 0 WITH
WAITUNTIL 70
-- Test 3: Governor reports bankruptcy promptly
`bankruptcy matter` MEANS Bankruptcy (Date 1 7 2024)
#TRACE `governor reporting obligation` `John Smith` `bankruptcy matter` AT 0 WITH
PARTY `the governor` `John Smith` DOES `report reportable matter` `bankruptcy matter` AT 10
-- Test 4: Governor fails to report, commissioner may suspend
#TRACE `governor reporting obligation` `John Smith` `bankruptcy matter` AT 0 WITH
WAITUNTIL 20
-- ============================================================
§ `Evaluations`
-- ============================================================
-- Check if Acme Animal Shelter meets the charity test
#EVAL `meets charity test` `Acme Animal Shelter`
-- Check public benefit
#EVAL `provides public benefit` `Acme Animal Shelter`
-- Check if animal welfare purpose was valid in 2024
#EVAL `purpose valid at date` `advancement of animal welfare` (Date 1 6 2024)
-- Check if animal welfare purpose is valid in 2025
#EVAL `purpose valid at date` `advancement of animal welfare` (Date 1 6 2025)
-- Check effect of registration event
`registration event` MEANS `charity registered` `Acme Animal Shelter` (Date 15 1 2024)
#EVAL `event effect` `registration event`
-- Check effect of late filing event
`late filing event` MEANS `annual return filed` `Acme Animal Shelter` 2024 TRUE
#EVAL `event effect` `late filing event`
: a charity registration scheme
-- Module A2: Cross-Cutting Concerns - Examples
-- This file demonstrates patterns for concerns that span multiple rules:
-- timing, notices, appeals, escalation, and grace periods.
--------------------------------------------------------------------------------
-- SECTION 1: Type Definitions
--------------------------------------------------------------------------------
-- Actor types for various procedures
DECLARE Actor IS ONE OF
`the Commissioner`
`the charity` HAS `the charity record` IS A `Registered Charity`
`the regulator`
`the appeal body`
`the Royal Court`
-- Separate party type for licence procedures
DECLARE `Licence Party` IS ONE OF
Holder HAS `the holder name` IS A STRING
-- Action types for regulatory procedures
DECLARE Action IS ONE OF
`take action`
`comply with requirement`
`issue warning notice` HAS `the violation` IS A STRING
`cure violation`
`impose penalty`
`serve Required Steps Notice`
`take required steps` HAS `the notice` IS A `Required Steps Notice`
`publish compliance`
`deregister charity`
`lodge appeal`
`determine appeal`
`lodge appeal against` HAS `the decision` IS A Decision
`determine appeal against` HAS `the decision` IS A Decision
`appeal to the Royal Court` HAS `the decision appealed` IS A `Commissioner Decision`
`decide the appeal` HAS `the outcome` IS A `Court Decision`
`withdraw the decision`
`make the varied decision` HAS `the varied decision` IS A Decision
`issue warning`
`comply with warning`
`impose fine`
`pay fine and comply`
`suspend registration`
`remedy and apply for reinstatement`
`remove from register`
`suspend immediately`
`pay` HAS `the payment amount` IS A NUMBER
`pay with late fee` HAS `the total amount` IS A NUMBER
-- Licence actions
DECLARE `Licence Action` IS ONE OF
`apply for renewal`
`apply with late fee`
`apply for reinstatement`
`lodge licence appeal`
-- Severity levels for violations
DECLARE Severity IS ONE OF
Minor
Serious
Critical
-- Violation record
DECLARE Violation
HAS `the description` IS A STRING
`the penalty` IS A NUMBER
`the severity` IS A Severity
-- Charity types
DECLARE `Charity Status` IS ONE OF
Active
Suspended
Dissolved
DECLARE `Registered Charity`
HAS `the charity name` IS A STRING
`the registration number` IS A STRING
`the status` IS A `Charity Status`
-- Decision types
DECLARE Decision
HAS `the decision id` IS A STRING
`the description` IS A STRING
DECLARE `Commissioner Decision`
HAS `the decision id` IS A STRING
`the decision type` IS A STRING
`the affected charity` IS A `Registered Charity`
-- Court decision outcomes
DECLARE `Court Decision` IS ONE OF
Upheld
Quashed
Varied HAS `the new decision` IS A Decision
-- Notice types
DECLARE `Required Steps Notice`
HAS `the notice id` IS A STRING
`the issued date` IS A NUMBER
`the steps` IS A LIST OF STRING
`the deadline` IS A NUMBER
-- Practicable deadline interpretations
DECLARE `Practicable Deadline` IS ONE OF
Immediate -- Within 24 hours
Prompt -- Within 7 days
Reasonable -- Within 14 days
Extended -- Within 30 days
--------------------------------------------------------------------------------
-- SECTION 2: Timing Patterns
--------------------------------------------------------------------------------
-- Convert "as soon as practicable" to specific day count
GIVEN timing IS A `Practicable Deadline`
GIVETH A NUMBER
`practicable days` MEANS
CONSIDER timing
WHEN Immediate THEN 1
WHEN Prompt THEN 7
WHEN Reasonable THEN 14
WHEN Extended THEN 30
-- Convert business days to calendar days (approximate)
-- 5 business days ≈ 7 calendar days
GIVEN `business days` IS A NUMBER
GIVETH A NUMBER
`to calendar days` MEANS (`business days` * 7) / 5
-- Example: 10 business days converted
`ten business days` MEANS `to calendar days` 10 -- ≈ 14 calendar days
--------------------------------------------------------------------------------
-- SECTION 3: Basic Deadline Obligations
--------------------------------------------------------------------------------
-- Simple deadline: fixed number of days
GIVEN party IS A Actor
action IS A Action
deadline IS A NUMBER
GIVETH A DEONTIC Actor Action
`obligation within days` MEANS
PARTY party
MUST action
WITHIN deadline
HENCE FULFILLED
LEST BREACH
-- Relative deadline: within N days after a trigger event
GIVEN party IS A Actor
action IS A Action
`the trigger date` IS A NUMBER -- Day number when trigger occurred
`the day limit` IS A NUMBER
GIVETH A DEONTIC Actor Action
`obligation after trigger` MEANS
PARTY party
MUST action
WITHIN (`the trigger date` + `the day limit`)
HENCE FULFILLED
LEST BREACH
--------------------------------------------------------------------------------
-- SECTION 4: Notice-and-Cure Pattern
--------------------------------------------------------------------------------
-- Generic notice-and-cure: violation detected, notice issued, cure period,
-- then consequence if not cured
GIVEN regulator IS A Actor
regulated IS A Actor
violation IS A STRING
`the cure period` IS A NUMBER
`the consequence` IS A Action
GIVETH A DEONTIC Actor Action
`notice and cure` MEANS
PARTY regulator
MAY `issue warning notice` violation
HENCE
PARTY regulated
MUST `cure violation`
WITHIN `the cure period`
HENCE FULFILLED
LEST
PARTY regulator
MAY `the consequence`
HENCE BREACH BY regulated BECAUSE "failed to cure violation"
-- If notice not issued, no further action required
--------------------------------------------------------------------------------
-- SECTION 5: Required Steps Notice (Jersey Charities Law Example)
--------------------------------------------------------------------------------
-- Article 27: Required Steps Notice procedure
GIVEN charity IS A `Registered Charity`
notice IS A `Required Steps Notice`
GIVETH A DEONTIC Actor Action
`required steps procedure` MEANS
-- Commissioner issues notice
PARTY `the Commissioner`
MUST `serve Required Steps Notice`
WITHIN 30
HENCE (
-- Charity must comply
PARTY `the charity` charity
MUST `take required steps` notice
WITHIN notice's `the deadline`
HENCE
-- If complied, Commissioner MUST publish
PARTY `the Commissioner`
MUST `publish compliance`
WITHIN 14
HENCE FULFILLED
LEST BREACH BY `the Commissioner` BECAUSE "failed to publish compliance"
LEST
-- If not complied, Commissioner MAY deregister
PARTY `the Commissioner`
MAY `deregister charity`
HENCE BREACH BY (`the charity` charity) BECAUSE "failed to take required steps"
)
LEST
BREACH BY `the Commissioner` BECAUSE "failed to serve notice"
--------------------------------------------------------------------------------
-- SECTION 6: Appeal Procedures
--------------------------------------------------------------------------------
-- Standard appeal pattern
DECLARE `Appeal Outcome` IS ONE OF
`appeal allowed`
`appeal dismissed`
`appeal partially allowed` HAS `the modifications` IS A STRING
-- Right to appeal with deadline
GIVEN appellant IS A Actor
`the appeal deadline` IS A NUMBER
GIVETH A DEONTIC Actor Action
`right to appeal` MEANS
PARTY appellant
MAY `lodge appeal`
WITHIN `the appeal deadline`
HENCE
-- Appeal body must decide
PARTY `the appeal body`
MUST `determine appeal`
WITHIN 90 -- Typical statutory deadline
HENCE FULFILLED
LEST BREACH BY `the appeal body` BECAUSE "failed to determine appeal in time"
-- Appeal with suspension effect
GIVEN decision IS A Decision
appellant IS A Actor
`the appeal deadline` IS A NUMBER
GIVETH A DEONTIC Actor Action
`suspensive appeal` MEANS
PARTY appellant
MAY `lodge appeal against` decision
WITHIN `the appeal deadline`
HENCE
-- Appeal must be determined
PARTY `the appeal body`
MUST `determine appeal against` decision
WITHIN 90
HENCE FULFILLED
LEST BREACH BY `the appeal body` BECAUSE "failed to determine appeal"
--------------------------------------------------------------------------------
-- SECTION 7: Article 33 - Appeal to Royal Court (Jersey Charities Law)
--------------------------------------------------------------------------------
-- What the Royal Court's decision leads to
GIVEN outcome IS A `Court Decision`
GIVETH A DEONTIC Actor Action
`the effect of the court's decision` MEANS
CONSIDER outcome
WHEN Upheld THEN FULFILLED
WHEN Quashed THEN
PARTY `the Commissioner`
MUST `withdraw the decision`
WITHIN 7
WHEN Varied `the new decision` THEN
PARTY `the Commissioner`
MUST `make the varied decision` (EXACTLY `the new decision`)
WITHIN 7
-- Article 33: Appeal Commissioner decision to Royal Court
GIVEN charity IS A `Registered Charity`
decision IS A `Commissioner Decision`
GIVETH A DEONTIC Actor Action
`appeal commissioner decision` MEANS
PARTY `the charity` charity
MAY `appeal to the Royal Court` (EXACTLY decision)
WITHIN 21 -- 21 days from notification
HENCE
-- No statutory deadline for the hearing, so no WITHIN
PARTY `the Royal Court`
MUST `decide the appeal` outcome
HENCE `the effect of the court's decision` outcome
--------------------------------------------------------------------------------
-- SECTION 8: Escalation Chains
--------------------------------------------------------------------------------
-- Escalation: Warning → Fine → Suspension → Removal
GIVEN subject IS A Actor
GIVETH A DEONTIC Actor Action
`escalation chain` MEANS
-- Level 1: Warning
PARTY `the regulator`
MAY `issue warning`
HENCE
PARTY subject
MUST `comply with warning`
WITHIN 30
HENCE FULFILLED
LEST
-- Level 2: Fine
PARTY `the regulator`
MAY `impose fine`
HENCE
PARTY subject
MUST `pay fine and comply`
WITHIN 14
HENCE FULFILLED
LEST
-- Level 3: Suspension
PARTY `the regulator`
MAY `suspend registration`
HENCE
PARTY subject
MUST `remedy and apply for reinstatement`
WITHIN 60
HENCE FULFILLED
LEST
-- Level 4: Removal
PARTY `the regulator`
MUST `remove from register`
HENCE BREACH
-- Escalation with bypass for serious violations
GIVEN violation IS A Violation
subject IS A Actor
GIVETH A DEONTIC Actor Action
`enforcement response` MEANS
IF violation's `the severity` EQUALS Critical
THEN
-- Immediate suspension for critical violations
PARTY `the regulator`
MUST `suspend immediately`
HENCE FULFILLED
LEST BREACH BY `the regulator` BECAUSE "failed to suspend critical violation"
ELSE IF violation's `the severity` EQUALS Serious
THEN
-- Skip warning for serious violations, go straight to fine
PARTY `the regulator`
MAY `impose fine`
HENCE
PARTY subject
MUST `pay fine and comply`
WITHIN 14
HENCE FULFILLED
LEST BREACH BY subject BECAUSE "failed to pay fine"
ELSE
-- Start with warning for minor violations
`escalation chain` subject
--------------------------------------------------------------------------------
-- SECTION 9: Grace Periods
--------------------------------------------------------------------------------
-- Payment with grace period before late fee applies
GIVEN debtor IS A Actor
amount IS A NUMBER
`the due date` IS A NUMBER
`the grace period` IS A NUMBER
`the late fee rate` IS A NUMBER
GIVETH A DEONTIC Actor Action
`payment with grace` MEANS
PARTY debtor
MUST `pay` amount
WITHIN `the due date`
HENCE FULFILLED
LEST
-- Grace period with late fee
PARTY debtor
MUST `pay with late fee` `the late amount`
WITHIN `the grace period`
HENCE FULFILLED
LEST BREACH BY debtor BECAUSE "failed to pay within grace period"
WHERE
`the late amount` MEANS amount * (1 + `the late fee rate`)
--------------------------------------------------------------------------------
-- SECTION 10: Licence Renewal Procedure (Exercise Solution)
--------------------------------------------------------------------------------
-- Complete licence renewal procedure with:
-- 1. Apply 30 days before expiry
-- 2. 14-day grace period with late fee
-- 3. Suspension after grace period
-- 4. 60-day reinstatement window
-- 5. Revocation with 21-day appeal right
-- Placeholder functions for licence status changes
`licence suspended` MEANS FULFILLED
`licence revoked` MEANS FULFILLED
`appeal procedure` MEANS FULFILLED
GIVEN holder IS A `Licence Party`
`the expiry date` IS A NUMBER
GIVETH A DEONTIC `Licence Party` `Licence Action`
`licence renewal procedure` MEANS
PARTY holder
MUST `apply for renewal`
WITHIN (`the expiry date` - 30) -- 30 days before expiry
HENCE FULFILLED
LEST
-- Grace period with late fee
PARTY holder
MUST `apply with late fee`
WITHIN 14 -- 14 day grace period, from when the first deadline is missed
HENCE FULFILLED
LEST
-- Reinstatement period after suspension
-- DO: an option. Doing it leads to HENCE, letting the time pass to LEST.
-- (A MAY would never reach its LEST.)
PARTY holder
DO `apply for reinstatement`
WITHIN 60
HENCE FULFILLED
LEST
-- Revocation with appeal right
PARTY holder
MAY `lodge licence appeal`
WITHIN 21
HENCE FULFILLED
-- If no appeal filed, licence is revoked
--------------------------------------------------------------------------------
-- SECTION 11: Test Cases
--------------------------------------------------------------------------------
-- Test charity for examples
`the test charity` MEANS `Registered Charity` "Test Charity" "TC-001" Active
-- Test notice
`the test notice` MEANS `Required Steps Notice` "RSN-001" 0 (LIST "Update records", "Submit report") 30
-- Test violations
`a minor violation` MEANS Violation "Late filing" 500 Minor
`a serious violation` MEANS Violation "Missing records" 2000 Serious
`a critical violation` MEANS Violation "Fraud detected" 10000 Critical
-- Test 1: Basic deadline obligation fulfilled
#TRACE `obligation within days` `the Commissioner` `take action` 14 AT 0 WITH
PARTY `the Commissioner` DOES `take action` AT 10
-- Test 2: Basic deadline obligation breached
#TRACE `obligation within days` `the Commissioner` `take action` 14 AT 0 WITH
PARTY `the Commissioner` DOES `take action` AT 20
-- Test 3: Required steps procedure - charity complies
#TRACE `required steps procedure` `the test charity` `the test notice` AT 0 WITH
PARTY `the Commissioner` DOES `serve Required Steps Notice` AT 1
PARTY (`the charity` `the test charity`) DOES `take required steps` `the test notice` AT 20
PARTY `the Commissioner` DOES `publish compliance` AT 30
-- Test 4: Required steps procedure - charity fails to comply
#TRACE `required steps procedure` `the test charity` `the test notice` AT 0 WITH
PARTY `the Commissioner` DOES `serve Required Steps Notice` AT 1
PARTY `the Commissioner` DOES `deregister charity` AT 40
-- Test 5: Payment with grace period - paid on time
#TRACE `payment with grace` `the Commissioner` 1000 30 10 0.1 AT 0 WITH
PARTY `the Commissioner` DOES `pay` 1000 AT 25
-- Test 6: Payment with grace period - the payment on day 32 misses the
-- 30-day deadline and opens the 10-day grace period; the payment with the
-- late fee on day 38 is within it
#TRACE `payment with grace` `the Commissioner` 1000 30 10 0.1 AT 0 WITH
PARTY `the Commissioner` DOES `pay` 1000 AT 32
PARTY `the Commissioner` DOES `pay with late fee` 1100 AT 38
-- Test 7: Escalation chain - complies at warning stage
#TRACE `escalation chain` `the Commissioner` AT 0 WITH
PARTY `the regulator` DOES `issue warning` AT 1
PARTY `the Commissioner` DOES `comply with warning` AT 20
-- Test 8: Enforcement response for minor violation
#TRACE `enforcement response` `a minor violation` `the Commissioner` AT 0 WITH
PARTY `the regulator` DOES `issue warning` AT 1
PARTY `the Commissioner` DOES `comply with warning` AT 20
-- Test 9: Enforcement response for critical violation
#TRACE `enforcement response` `a critical violation` `the Commissioner` AT 0 WITH
PARTY `the regulator` DOES `suspend immediately` AT 1
-- Test 10: Licence renewal - on time
`the test holder` MEANS Holder "Test Holder"
#TRACE `licence renewal procedure` `the test holder` 100 AT 0 WITH
PARTY `the test holder` DOES `apply for renewal` AT 60
-- Test 11: Licence renewal - late with fee: the application on day 75 misses
-- the day-70 deadline and opens the 14-day grace period; the late-fee
-- application on day 80 is within it
#TRACE `licence renewal procedure` `the test holder` 100 AT 0 WITH
PARTY `the test holder` DOES `apply for renewal` AT 75
PARTY `the test holder` DOES `apply with late fee` AT 80
-- Test 12: Licence renewal - reinstatement: both deadlines are missed
-- (day 75, then day 95), and the holder applies for reinstatement on day 100
#TRACE `licence renewal procedure` `the test holder` 100 AT 0 WITH
PARTY `the test holder` DOES `apply for renewal` AT 75
PARTY `the test holder` DOES `apply with late fee` AT 95
PARTY `the test holder` DOES `apply for reinstatement` AT 100
-- Test 13: Article 33 appeal - the Royal Court quashes the decision,
-- and the Commissioner withdraws it within 7 days
`the test decision` MEANS `Commissioner Decision` "CD-001" "deregistration" `the test charity`
#TRACE `appeal commissioner decision` `the test charity` `the test decision` AT 0 WITH
PARTY (`the charity` `the test charity`) DOES `appeal to the Royal Court` `the test decision` AT 10
PARTY `the Royal Court` DOES `decide the appeal` Quashed AT 60
PARTY `the Commissioner` DOES `withdraw the decision` AT 62
-- Test 14: Article 33 appeal - the Royal Court varies the decision; the
-- result is the Commissioner's duty to make the varied decision
`the varied test decision` MEANS Decision "CD-001-V" "suspension for 3 months"
#TRACE `appeal commissioner decision` `the test charity` `the test decision` AT 0 WITH
PARTY (`the charity` `the test charity`) DOES `appeal to the Royal Court` `the test decision` AT 10
PARTY `the Royal Court` DOES `decide the appeal` (Varied `the varied test decision`) AT 60
: timing, notices, appeals and escalation
-- Module A3: Contracts in Depth - Examples
-- This file demonstrates advanced contract modeling including complex payment terms,
-- recursive obligations, and penalty structures.
--------------------------------------------------------------------------------
-- SECTION 1: Type Definitions
--------------------------------------------------------------------------------
-- Money type with currency
DECLARE Money
HAS `the amount` IS A NUMBER
`the currency` IS A STRING
-- Currency constructors
GIVEN n IS A NUMBER
GIVETH A Money
USD MEANS Money WITH `the amount` IS n, `the currency` IS "USD"
GIVEN n IS A NUMBER
GIVETH A Money
SGD MEANS Money WITH `the amount` IS n, `the currency` IS "SGD"
-- Person and Company types (basic definitions)
DECLARE Person
HAS `the name` IS A STRING
DECLARE Company
HAS `the name` IS A STRING
-- Party types
DECLARE Party IS ONE OF
`the borrower party` HAS `the borrower` IS A Borrower
`the lender party` HAS `the lender` IS A Lender
-- Borrower can be individual or company
DECLARE Borrower IS ONE OF
`individual borrower` HAS `the person` IS A Person
`corporate borrower` HAS `the company` IS A Company
DECLARE Lender IS ONE OF
`individual lender` HAS `the person` IS A Person
`institutional lender` HAS `the company` IS A Company
-- Payment record
DECLARE Payment
HAS `the amount` IS A Money
`the due date` IS A NUMBER -- Days from commencement
-- Penalty terms
DECLARE `Penalty Terms`
HAS `the penalty rate` IS A NUMBER
`the grace period` IS A NUMBER -- in days
--------------------------------------------------------------------------------
-- SECTION 2: Loan Terms
--------------------------------------------------------------------------------
DECLARE `Loan Terms`
HAS `the principal` IS A Money
`the annual interest rate` IS A NUMBER
`the number of installments` IS A NUMBER
`the days until default` IS A NUMBER
`the penalty terms` IS A `Penalty Terms`
-- Example loan
`the example loan` MEANS `Loan Terms` WITH
`the principal` IS USD 25000
`the annual interest rate` IS 0.15 -- 15% annual interest
`the number of installments` IS 12 -- 12 monthly installments
`the days until default` IS 30 -- Default after 30 days late
`the penalty terms` IS `Penalty Terms` WITH
`the penalty rate` IS 0.05 -- 5% penalty
`the grace period` IS 10
--------------------------------------------------------------------------------
-- SECTION 3: Payment Calculations
--------------------------------------------------------------------------------
-- Monthly interest rate
GIVEN terms IS A `Loan Terms`
GIVETH A NUMBER
`monthly rate` MEANS terms's `the annual interest rate` / 12
-- Power function for calculations
GIVEN base IS A NUMBER
exp IS A NUMBER
GIVETH A NUMBER
`power` MEANS
IF exp = 0
THEN 1
ELSE IF exp = 1
THEN base
ELSE base * `power` base (exp - 1)
-- Monthly payment using amortization formula
-- PMT = P × (r(1+r)^n) / ((1+r)^n - 1)
GIVEN terms IS A `Loan Terms`
GIVETH A Money
`monthly payment amount` MEANS
Money WITH `the amount` IS payment, `the currency` IS terms's `the principal`'s `the currency`
WHERE
p MEANS terms's `the principal`'s `the amount`
r MEANS `monthly rate` terms
n MEANS terms's `the number of installments`
`the compound factor` MEANS `power` (1 + r) n
payment MEANS p * (r * `the compound factor`) / (`the compound factor` - 1)
-- Placeholder functions for payment scheduling
GIVEN terms IS A `Loan Terms`
outstanding IS A Money
GIVETH A Money
`calculate next payment` MEANS `monthly payment amount` terms
GIVEN terms IS A `Loan Terms`
outstanding IS A Money
GIVETH A NUMBER
`calculate due date` MEANS 30 -- Simplified: 30 days between payments
--------------------------------------------------------------------------------
-- SECTION 4: Loan Contract Actions
--------------------------------------------------------------------------------
-- Actions for the loan contract
DECLARE `Loan Action` IS ONE OF
`pay installment` HAS `the recipient` IS A Lender
`the amount` IS A Money
-- Validate payment amount
GIVEN paid IS A Money
expected IS A Money
GIVETH A BOOLEAN
`is valid payment` MEANS
paid's `the currency` EQUALS expected's `the currency`
AND paid's `the amount` >= (expected's `the amount` - 0.05) -- Allow small rounding
--------------------------------------------------------------------------------
-- SECTION 5: Recursive Payment Obligations
--------------------------------------------------------------------------------
-- Test borrower and lender for examples
`Alice the borrower` MEANS `individual borrower` (Person WITH `the name` IS "Alice")
`Bob the lender` MEANS `individual lender` (Person WITH `the name` IS "Bob")
-- The recursive payment obligation
GIVEN terms IS A `Loan Terms`
debtor IS A Borrower
creditor IS A Lender
outstanding IS A Money -- Remaining balance
GIVETH A DEONTIC Party `Loan Action`
`payment obligation` MEANS
IF outstanding's `the amount` > 0
THEN
PARTY `the borrower party` debtor
MUST `pay installment` EXACTLY creditor
`the amount paid` PROVIDED `the amount paid`'s `the amount` >= `the payment due`'s `the amount`
WITHIN `the next due date`
HENCE
-- Recursive call with reduced balance
`payment obligation` terms debtor creditor `the new outstanding balance`
LEST
-- Late: apply penalty
`late payment handling` terms debtor creditor outstanding
ELSE FULFILLED
WHERE
-- Calculate next payment
`the payment due` MEANS `calculate next payment` terms outstanding
`the next due date` MEANS `calculate due date` terms outstanding
-- After payment, reduce outstanding (simplified)
`the new outstanding balance` MEANS Money WITH
`the amount` IS outstanding's `the amount` - `the payment due`'s `the amount`
`the currency` IS outstanding's `the currency`
-- Late payment with penalty
GIVEN terms IS A `Loan Terms`
debtor IS A Borrower
creditor IS A Lender
outstanding IS A Money
GIVETH A DEONTIC Party `Loan Action`
`late payment handling` MEANS
-- Grace period with penalty interest
PARTY `the borrower party` debtor
MUST `pay installment` EXACTLY creditor
`the amount paid` PROVIDED `the amount paid`'s `the amount` >= `the payment with penalty`'s `the amount`
WITHIN (`the next due date` + terms's `the penalty terms`'s `the grace period`)
HENCE
-- Continue with remaining payments
`payment obligation` terms debtor creditor `the new outstanding balance`
LEST
-- Default: full balance due
`default handling` terms debtor creditor outstanding
WHERE
`the base payment` MEANS `calculate next payment` terms outstanding
`the penalty amount` MEANS `the base payment`'s `the amount` * terms's `the penalty terms`'s `the penalty rate`
`the payment with penalty` MEANS Money WITH
`the amount` IS `the base payment`'s `the amount` + `the penalty amount`
`the currency` IS `the base payment`'s `the currency`
`the next due date` MEANS `calculate due date` terms outstanding
`the new outstanding balance` MEANS Money WITH
`the amount` IS outstanding's `the amount` - `the payment with penalty`'s `the amount`
`the currency` IS outstanding's `the currency`
-- Default: Full balance due
GIVEN terms IS A `Loan Terms`
debtor IS A Borrower
creditor IS A Lender
outstanding IS A Money
GIVETH A DEONTIC Party `Loan Action`
`default handling` MEANS
PARTY `the borrower party` debtor
MUST `pay installment` EXACTLY creditor
EXACTLY outstanding -- Full balance required
WITHIN terms's `the days until default`
HENCE FULFILLED
LEST BREACH BY (`the borrower party` debtor) BECAUSE "loan default"
--------------------------------------------------------------------------------
-- SECTION 6: Multi-Party Contracts (Escrow)
--------------------------------------------------------------------------------
-- Escrow arrangement: Buyer, Seller, Escrow Agent
DECLARE `Escrow Party` IS ONE OF `the buyer`, `the seller`, `the escrow agent`
DECLARE `Escrow Action` IS ONE OF
`deposit funds` HAS `the amount` IS A Money
`deliver goods`
`release funds to seller`
`return funds to buyer`
GIVEN amount IS A Money
GIVETH A DEONTIC `Escrow Party` `Escrow Action`
`escrow arrangement` MEANS
-- Buyer deposits funds
PARTY `the buyer`
MUST `deposit funds` amount
WITHIN 7
HENCE
-- Seller delivers goods
PARTY `the seller`
MUST `deliver goods`
WITHIN 14
HENCE
-- Escrow releases to seller
PARTY `the escrow agent`
MUST `release funds to seller`
WITHIN 3
HENCE FULFILLED
LEST BREACH BY `the escrow agent` BECAUSE "escrow agent failed to release funds"
LEST
-- Seller didn't deliver, return funds
PARTY `the escrow agent`
MUST `return funds to buyer`
WITHIN 3
HENCE BREACH BY `the seller` BECAUSE "seller failed to deliver goods"
LEST BREACH BY `the escrow agent` BECAUSE "escrow agent failed to return funds"
LEST BREACH BY `the buyer` BECAUSE "buyer failed to deposit funds"
--------------------------------------------------------------------------------
-- SECTION 7: Parallel and Alternative Obligations
--------------------------------------------------------------------------------
-- Types for service contract examples
DECLARE `Service Party` IS ONE OF Provider, Client
DECLARE `Contract Action` IS ONE OF
`deliver service`
`provide documentation`
`ship goods`
`arrange pickup`
`make payment`
-- Parallel obligations with RAND
-- Service contract: Provider must deliver service AND provide documentation
GIVETH A DEONTIC `Service Party` `Contract Action`
`service delivery` MEANS
(PARTY Provider MUST `deliver service` WITHIN 30 HENCE FULFILLED LEST BREACH BY Provider BECAUSE "failed to deliver service")
RAND
(PARTY Provider MUST `provide documentation` WITHIN 30 HENCE FULFILLED LEST BREACH BY Provider BECAUSE "failed to provide documentation")
-- Alternative obligations with ROR
-- Delivery options: Ship OR pickup
GIVETH A DEONTIC `Service Party` `Contract Action`
`delivery options` MEANS
(PARTY Provider MUST `ship goods` WITHIN 14 HENCE FULFILLED LEST BREACH BY Provider BECAUSE "failed to ship")
ROR
(PARTY Provider MUST `arrange pickup` WITHIN 7 HENCE FULFILLED LEST BREACH BY Provider BECAUSE "failed to arrange pickup")
--------------------------------------------------------------------------------
-- SECTION 8: Practical Patterns
--------------------------------------------------------------------------------
-- Credit card style: Pay minimum or full balance
DECLARE `Card Party` IS ONE OF Cardholder, Bank
DECLARE `Card Action` IS ONE OF
`pay` HAS `the payment amount` IS A NUMBER
GIVEN balance IS A Money
`the minimum percentage` IS A NUMBER
GIVETH A DEONTIC `Card Party` `Card Action`
`credit payment` MEANS
PARTY Cardholder
MUST `pay` `the amount paid` PROVIDED `the amount paid` >= `the minimum payment`
WITHIN 30
HENCE
IF `the amount paid` >= balance's `the amount`
THEN FULFILLED -- Paid in full
ELSE `credit payment` `the new balance` `the minimum percentage` -- Recurse with new balance
LEST BREACH BY Cardholder BECAUSE "missed credit card payment"
WHERE
`the minimum payment` MEANS balance's `the amount` * `the minimum percentage`
`the new balance` MEANS Money WITH `the amount` IS balance's `the amount` - `the minimum payment`, `the currency` IS balance's `the currency`
-- Milestone-based payment pattern
DECLARE Milestone IS ONE OF
Design
Development
Testing
Delivery
DECLARE `Milestone Action` IS ONE OF
`complete milestone` HAS `the completed milestone` IS A Milestone
`pay milestone` HAS `the paid milestone` IS A Milestone
GIVEN milestones IS A LIST OF Milestone
GIVETH A DEONTIC `Service Party` `Milestone Action`
`milestone payments` MEANS
CONSIDER milestones
WHEN EMPTY THEN FULFILLED
WHEN m FOLLOWED BY rest THEN
PARTY Provider
MUST `complete milestone` m
WITHIN 30
HENCE
PARTY Client
MUST `pay milestone` m
WITHIN 14
HENCE `milestone payments` rest -- Recurse
LEST BREACH BY Client BECAUSE "client failed to pay milestone"
LEST BREACH BY Provider BECAUSE "provider failed to complete milestone"
--------------------------------------------------------------------------------
-- SECTION 9: Security Deposit (Exercise Solution)
--------------------------------------------------------------------------------
-- Exercise: at the end of the lease, the landlord must either refund the
-- deposit in full within 14 days, or send an itemized list of deductions
-- within 7 days and refund the balance within 21 days.
DECLARE `Tenancy Party` IS ONE OF
`the landlord`
`the tenant`
DECLARE `Tenancy Action` IS ONE OF
`refund the deposit in full`
`send an itemized list of deductions`
`refund the balance`
GIVETH A DEONTIC `Tenancy Party` `Tenancy Action`
`deposit return obligation` MEANS
(PARTY `the landlord`
MUST `refund the deposit in full`
WITHIN 14
HENCE FULFILLED
LEST BREACH BY `the landlord` BECAUSE "failed to refund the deposit")
ROR
(PARTY `the landlord`
MUST `send an itemized list of deductions`
WITHIN 7
HENCE
PARTY `the landlord`
MUST `refund the balance`
WITHIN 21
HENCE FULFILLED
LEST BREACH BY `the landlord` BECAUSE "failed to refund the balance"
LEST BREACH BY `the landlord` BECAUSE "failed to account for deductions")
--------------------------------------------------------------------------------
-- SECTION 10: Test Traces
--------------------------------------------------------------------------------
-- Escrow: happy path
#TRACE `escrow arrangement` (USD 5000) AT 0 WITH
PARTY `the buyer` DOES `deposit funds` (USD 5000) AT 2
PARTY `the seller` DOES `deliver goods` AT 10
PARTY `the escrow agent` DOES `release funds to seller` AT 12
-- Escrow: seller fails to deliver, funds returned
#TRACE `escrow arrangement` (USD 5000) AT 0 WITH
PARTY `the buyer` DOES `deposit funds` (USD 5000) AT 2
WAITUNTIL 17
PARTY `the escrow agent` DOES `return funds to buyer` AT 18
-- Milestones: first milestone completed and paid
#TRACE `milestone payments` (LIST Design, Development) AT 0 WITH
PARTY Provider DOES `complete milestone` Design AT 10
PARTY Client DOES `pay milestone` Design AT 20
PARTY Provider DOES `complete milestone` Development AT 45
PARTY Client DOES `pay milestone` Development AT 55
-- Deposit return: full refund on time
#TRACE `deposit return obligation` AT 0 WITH
PARTY `the landlord` DOES `refund the deposit in full` AT 10
-- Deposit return: itemized deductions then balance refunded
#TRACE `deposit return obligation` AT 0 WITH
PARTY `the landlord` DOES `send an itemized list of deductions` AT 5
PARTY `the landlord` DOES `refund the balance` AT 20
--------------------------------------------------------------------------------
-- SECTION 11: Evaluations
--------------------------------------------------------------------------------
-- Monthly payment for the example loan (expected: approximately 2256.45)
#EVAL `monthly payment amount` `the example loan`
-- Payment validation
#EVAL `is valid payment` (USD 2256.44) (USD 2256.45) -- TRUE (within rounding)
#EVAL `is valid payment` (USD 2200) (USD 2256.45) -- FALSE (short)
#EVAL `is valid payment` (SGD 2256.45) (USD 2256.45) -- FALSE (wrong currency)
: a loan contract with recursive obligations
More real-world encodings, including a complete promissory note, are in the legal examples of the L4 repository.
After this course
For a specific task, see the Tutorials; for the theory behind L4, Concepts. Then apply what you have learned to the rules of your own domain.