Advanced Course
Deep dives into complex L4 patterns for production use.
Overview
This course covers advanced techniques for modeling complex legal systems:
- Real regulatory schemes with multiple instruments
- Cross-cutting concerns (timing, notices, appeals)
- Multi-temporal reasoning
- Production patterns and debugging
Prerequisites: Completion of the Foundation Course
Modules
Module A1: Real Regulatory Schemes
Model complete legislative frameworks.
- The three-layer approach (structural, deontic, events)
- Encoding definitions from legislation
- Handling cross-references
- Building from a real example: charity regulation
Module A2: Cross-Cutting Concerns
Patterns that span multiple rules.
- Timing and deadlines
- Notice requirements
- Appeal procedures
- Grace periods and escalation
Module A3: Contracts in Depth
Advanced contract modeling.
- Complex payment terms
- Recursive obligations
- Penalty structures
- Real-world example: promissory note
Module A4: Production Patterns
Patterns for robust, maintainable code.
- Organizing large codebases
- Testing strategies
- Common debugging patterns
- Integration considerations
Learning Path
Complete modules in order:
Foundation Course ──► Module A1 ──► Module A2 ──► Module A3 ──► Module A4
Example Code
Each module ships 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
(`WAIT UNTIL` 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
(`WAIT UNTIL` 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`
- 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
`hear appeal` HAS `the decision` IS A `Commissioner 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)
--------------------------------------------------------------------------------
-- Placeholder functions for court decisions
`original decision takes effect` MEANS FULFILLED
`decision has no effect` MEANS FULFILLED
GIVEN `the new decision` IS A Decision
GIVETH A DEONTIC Actor Action
`varied decision takes effect` MEANS FULFILLED
-- 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 `hear appeal` decision -- Note: using available action
WITHIN 21 -- 21 days from notification
HENCE
PARTY `the Royal Court`
MUST `hear appeal` decision
-- No statutory deadline for hearing in original law
HENCE FULFILLED
LEST BREACH BY `the Royal Court` BECAUSE "failed to hear appeal"
--------------------------------------------------------------------------------
-- 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 deadline`
HENCE FULFILLED
LEST BREACH BY debtor BECAUSE "failed to pay within grace period"
WHERE
`the late amount` MEANS amount * (1 + `the late fee rate`)
`the grace deadline` MEANS `the due date` + `the grace period`
--------------------------------------------------------------------------------
-- 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 (`the expiry date` - 30 + 14) -- 14 day grace period
HENCE FULFILLED
LEST
-- Reinstatement period after suspension
PARTY holder
MAY `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 - paid during grace
#TRACE `payment with grace` `the Commissioner` 1000 30 10 0.1 AT 0 WITH
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
#TRACE `licence renewal procedure` `the test holder` 100 AT 0 WITH
PARTY `the test holder` DOES `apply with late fee` AT 78
-- Test 12: Licence renewal - reinstatement
#TRACE `licence renewal procedure` `the test holder` 100 AT 0 WITH
PARTY `the test holder` DOES `apply for reinstatement` AT 100
- Timing, notices, appeals, 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
(`WAIT UNTIL` 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)
- Loan contract with recursive obligations
Related real-world encodings in the repository:
jl4/examples/legal/promissory-note.l4- Complete loan agreementjl4/examples/legal/- Other real-world examples
After This Course
Continue learning with: