-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathreference_surface.hum
More file actions
182 lines (135 loc) · 3.22 KB
/
Copy pathreference_surface.hum
File metadata and controls
182 lines (135 loc) · 3.22 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
module examples.reference_surface
app reference_surface {
why:
show every current Milestone 0 top-level form in one checked file
starts with:
start_reference
task start_reference -> Unit {
why:
keep the reference app structurally executable without external effects
does:
return
}
}
type WorkItem {
id: Text
title: Text
done: Bool
}
type WorkError {
code: Text
}
store work_items: list WorkItem {
why:
keep the user's work items available between tasks
}
task remember_work_item(title: Text) -> Result WorkItem, WorkError {
why:
let a user capture work without losing the reason it matters
# comments inside sections are preserved as section facts
targets:
triple: wasm32-wasi-preview1
requires: os.clock
requires: os.filesystem
denies: os.network
uses:
clock
changes:
work_items
needs:
title is not empty
ensures:
new work item is saved
new work item is not done
protects:
user work history
trusts:
local profile storage
fails when:
title is empty
watch for:
title may contain only spaces
cost:
time: O(1)
space: O(1)
check: warn
allocates:
one work item
avoids:
saving empty work items
tradeoffs:
local persistence is enough for the reference surface
optimizes:
clear review facts over clever implementation
tests:
remember_work_item rejects empty title
does:
if title is empty {
fail WorkError.empty_title
}
let item = WorkItem {
id: clock.now_text
title: title
done: false
}
save item in work_items
return item
}
test remember_work_item rejects empty title regression {
why:
prove the reference entry records its visible failure mode
uses:
remember_work_item
needs:
empty title input is available
regression:
empty titles used to be saved as blank work items
covers:
remember_work_item needs title is not empty
remember_work_item watch for title may contain only spaces
remember_work_item tests remember_work_item rejects empty title
avoids:
depending on real storage or network behavior
cost:
time: O(1)
space: O(1)
check: warn
does:
expect remember_work_item("") fails with WorkError.empty_title
}
test remember_work_item saves valid title unit {
why:
prove the reference entry records its success promises
uses:
remember_work_item
needs:
non-empty title input is available
covers:
remember_work_item ensures new work item is saved
remember_work_item ensures new work item is not done
avoids:
depending on real storage or network behavior
cost:
time: O(1)
space: O(1)
check: warn
does:
expect remember_work_item("ship Hum docs") returns WorkItem
}
test remember_work_item records security evidence unit {
why:
prove the reference entry records security and trust evidence links
uses:
remember_work_item
covers:
remember_work_item protects user work history
remember_work_item trusts local profile storage
avoids:
depending on real storage or network behavior
cost:
time: O(1)
space: O(1)
check: warn
does:
expect evidence links are present in graph output
}