例とチュートリアル

module TaskManager definitions types TaskId = nat1; Priority = <Low> | <Medium> | <High>; Status = <Todo> | <InProgress> | <Done>; Task :: id : TaskId title : seq1 of char desc : seq of char status : Status priority : Priority assignee : [seq1 of char] inv t == len t.title <= 100 and len t.desc <= 500; TaskBoard = map TaskId to Task inv board == forall id in set dom board & board(id).id = id; functions ValidTransition: Status * Status -> bool ValidTransition(fromSt, toSt) == if fromSt = toSt then true else if fromSt = <Done> then false else true; operations CreateTask: seq1 of char * seq of char * Priority * [seq1 of char] ==> TaskId CreateTask(title, desc, priority, assignee) == ... pre len title <= 100 and len desc <= 500 post RESULT in set dom board and board(RESULT).status = <Todo>; ChangeStatus: TaskId * Status ==> () ChangeStatus(taskId, newStatus) == ... pre taskId in set dom board and ValidTransition(board(taskId).status, newStatus) post board(taskId).status = newStatus; DeleteTask: TaskId ==> () DeleteTask(taskId) == ... pre taskId in set dom board post taskId not in set dom board and card dom board = card dom board~ - 1; end TaskManager

changeStatus(taskId: TaskId, newStatus: Status): void { // Pre-conditions (from VDM-SL) checkPre(this.board.has(taskId), `taskId ${taskId} not in dom board`); checkPre(validTransition(oldTask.status, newStatus), `Invalid transition: ${oldTask.status} → ${newStatus}`); const oldTitle = oldTask.title; const updated = mkTask(oldTask.id, oldTask.title, oldTask.desc, newStatus, oldTask.priority, oldTask.assignee); this.board.set(taskId, updated); // Post-conditions (from VDM-SL) checkPost(this.board.get(taskId)!.status === newStatus, `status must be ${newStatus}`); checkPost(this.board.get(taskId)!.title === oldTitle, `title must be preserved`); this.checkStateInvariant(); }

=== TaskManager: Integrated Workflow Smoke Test === --- 1. Task Creation --- ✓ CreateTask: 'Design API' (High, Alice) ✓ CreateTask: 'Write Tests' (Medium, Bob) ✓ CreateTask: empty title rejected ✓ CreateTask: title > 100 chars rejected ✓ CreateTask: desc > 500 chars rejected --- 2. Status Transitions --- ✓ ChangeStatus: Todo → InProgress ✓ ChangeStatus: InProgress → Done ✓ ChangeStatus: Done → InProgress rejected ✓ ChangeStatus: Done → Todo rejected ✓ ChangeStatus: Todo → Todo (no-op) --- 3. Update & Delete --- ✓ UpdateTask: title & priority changed, status preserved ✓ DeleteTask: board size decreased by 1 ✓ DeleteTask: already deleted taskId rejected --- 5. Board Summary --- ✓ GetSummary: counts match board size --- 7. Invariant Enforcement --- ✓ mkTask: TaskId=0 (nat1) rejected ✓ mkTask: empty title (seq1 of char) rejected === Results: 23 passed, 0 failed ===