LAWS.bend
qasim-bend-kit@0.1.0.1 · 273 lines · 0 definitions
1# Library correctness laws and integration obligations.
2
3import Base
4
5# JSON contract: libs/JSON.bend.
6#
7# Expected API:
8# Json.parse(text: String) -> Result<&1, &1, Json.Error, Json.Value>
9# Json.stringify(value: Json.Value) -> String
10
11import qasim-bend-kit@0.1.0.1/libs/JSON.bend as Json
12import qasim-bend-kit@0.1.0.1/libs/URL.bend as URL
13
14# ============================================================
15# JSON: Core correctness
16# ============================================================
17
18law stringify_parse_roundtrip:
19 for value: Json.Value {
20 Json.parse(Json.stringify(value))
21 ==
22 Done{value}
23 :
24 Result<&1, &1, Json.Error, Json.Value>
25 }
26
27# ============================================================
28# JSON: Literals
29# ============================================================
30
31law parses_null:
32 { Json.parse("null") == Done{Json.Null{}} :
33 Result<&1, &1, Json.Error, Json.Value> }
34
35law parses_true:
36 { Json.parse("true") == Done{Json.Bool{True{}}} :
37 Result<&1, &1, Json.Error, Json.Value> }
38
39law parses_false:
40 { Json.parse("false") == Done{Json.Bool{False{}}} :
41 Result<&1, &1, Json.Error, Json.Value> }
42
43# ============================================================
44# JSON: Whitespace
45# ============================================================
46
47law accepts_leading_space:
48 for value: Json.Value {
49 Json.parse(" " ++ Json.stringify(value)) == Done{value} :
50 Result<&1, &1, Json.Error, Json.Value>
51 }
52
53law accepts_trailing_space:
54 for value: Json.Value {
55 Json.parse(Json.stringify(value) ++ " ") == Done{value} :
56 Result<&1, &1, Json.Error, Json.Value>
57 }
58
59law accepts_surrounding_space:
60 for value: Json.Value {
61 Json.parse(" \n\t\r" ++ Json.stringify(value) ++ "\r\t\n ") == Done{value} :
62 Result<&1, &1, Json.Error, Json.Value>
63 }
64
65# ============================================================
66# JSON: Invalid and incomplete input
67# ============================================================
68
69law rejects_trailing_garbage:
70 { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("nullx"))
71 == True{} : Bool }
72
73law rejects_second_value:
74 { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("null true"))
75 == True{} : Bool }
76
77law rejects_invalid_null:
78 { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("nul"))
79 == True{} : Bool }
80
81law rejects_invalid_true:
82 { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("tru"))
83 == True{} : Bool }
84
85law rejects_invalid_false:
86 { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("fals"))
87 == True{} : Bool }
88
89law rejects_empty_input:
90 { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse(""))
91 == True{} : Bool }
92
93law rejects_whitespace_only:
94 { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse(" \t\r\n "))
95 == True{} : Bool }
96
97# ============================================================
98# JSON: Strings
99# ============================================================
100
101law parses_empty_string:
102 { Json.parse("\"\"") == Done{Json.Str{""}} :
103 Result<&1, &1, Json.Error, Json.Value> }
104
105law parses_simple_string:
106 { Json.parse("\"hello\"") == Done{Json.Str{"hello"}} :
107 Result<&1, &1, Json.Error, Json.Value> }
108
109law parses_newline_escape:
110 { Json.parse("\"a\\nb\"") == Done{Json.Str{"a\nb"}} :
111 Result<&1, &1, Json.Error, Json.Value> }
112
113law parses_quote_escape:
114 { Json.parse("\"a\\\"b\"") == Done{Json.Str{"a\"b"}} :
115 Result<&1, &1, Json.Error, Json.Value> }
116
117law parses_backslash_escape:
118 { Json.parse("\"a\\\\b\"") == Done{Json.Str{"a\\b"}} :
119 Result<&1, &1, Json.Error, Json.Value> }
120
121law rejects_unterminated_string:
122 { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("\"hello"))
123 == True{} : Bool }
124
125# ============================================================
126# JSON: Arrays
127# ============================================================
128
129law parses_empty_array:
130 { Json.parse("[]") == Done{Json.Arr{Nil{}}} :
131 Result<&1, &1, Json.Error, Json.Value> }
132
133law parses_literal_array:
134 {
135 Json.parse("[null,true,false]")
136 ==
137 Done{Json.Arr{
138 Json.Null{} <>
139 Json.Bool{True{}} <>
140 Json.Bool{False{}} <>
141 Nil{}
142 }}
143 :
144 Result<&1, &1, Json.Error, Json.Value>
145 }
146
147law rejects_array_trailing_comma:
148 { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("[null,]"))
149 == True{} : Bool }
150
151# ============================================================
152# JSON: Objects
153# ============================================================
154
155law parses_empty_object:
156 { Json.parse("{}") == Done{Json.Obj{Nil{}}} :
157 Result<&1, &1, Json.Error, Json.Value> }
158
159law rejects_unquoted_object_key:
160 { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("{foo:null}"))
161 == True{} : Bool }
162
163law rejects_object_trailing_comma:
164 { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("{\"x\":null,}"))
165 == True{} : Bool }
166
167# ============================================================
168# JSON: Nesting
169# ============================================================
170
171law parses_nested_containers:
172 {
173 Json.parse("[{\"x\":[true,null]}]")
174 ==
175 Done{Json.Arr{
176 Json.Obj{
177 ("x", Json.Arr{
178 Json.Bool{True{}} <>
179 Json.Null{} <>
180 Nil{}
181 }) <>
182 Nil{}
183 } <>
184 Nil{}
185 }}
186 :
187 Result<&1, &1, Json.Error, Json.Value>
188 }
189
190# ============================================================
191# JSON: Additional semantics
192# ============================================================
193
194# JSON permits only space, tab, carriage return and line feed as whitespace.
195law rejects_non_json_whitespace:
196 { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("\u{000b}null"))
197 == True{} : Bool }
198
199# A raw control character is forbidden inside a JSON string.
200law rejects_raw_string_control:
201 { Result.is_fail(&1, &1, Json.Error, Json.Value,
202 Json.parse("\"" ++ "\u{0001}" ++ "\""))
203 == True{} : Bool }
204
205# Unicode escapes decode to their scalar value, including a surrogate pair.
206law parses_unicode_escape:
207 { Json.parse("\"\\u263A\"") == Done{Json.Str{"\u{263a}"}} :
208 Result<&1, &1, Json.Error, Json.Value> }
209
210law parses_unicode_surrogate_pair:
211 { Json.parse("\"\\uD83D\\uDE00\"") == Done{Json.Str{"\u{1f600}"}} :
212 Result<&1, &1, Json.Error, Json.Value> }
213
214# This representative decimal/exponent form is accepted. A separate law below
215# checks that the smart number constructor preserves the original lexeme.
216law parses_fraction_and_exponent:
217 { Result.is_done(&1, &1, Json.Error, Json.Value, Json.parse("-12.50e+3"))
218 == True{} : Bool }
219
220law rejects_malformed_number_forms:
221 { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("01"))
222 && Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("1."))
223 && Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("1e+"))
224 == True{} : Bool }
225
226# Arrays retain source order. Objects retain source order and duplicate keys;
227# consumers that need map semantics must choose their own duplicate-key policy.
228law preserves_array_order:
229 { Json.parse("[3,1,2]") == Done{Json.Arr{
230 Json.Number{"3", Json.Certified{Json.number_proof("3", {==})}} <>
231 Json.Number{"1", Json.Certified{Json.number_proof("1", {==})}} <>
232 Json.Number{"2", Json.Certified{Json.number_proof("2", {==})}} <>
233 Nil{}
234 }} : Result<&1, &1, Json.Error, Json.Value> }
235
236law preserves_object_order_and_duplicates:
237 { Json.parse("{\"x\":1,\"x\":2}") == Done{Json.Obj{
238 ("x", Json.Number{"1", Json.Certified{Json.number_proof("1", {==})}}) <>
239 ("x", Json.Number{"2", Json.Certified{Json.number_proof("2", {==})}}) <>
240 Nil{}
241 }} : Result<&1, &1, Json.Error, Json.Value> }
242
243# GPU entry points have the same specified results as their CPU counterparts.
244law gpu_single_matches_cpu:
245 for text: String {
246 Json.parse_gpu(text) == Json.parse(text) :
247 Result<&1, &1, Json.Error, Json.Value>
248 }
249
250law preserves_number_lexeme:
251 { Json.number("-12.50e+3") == Done{Json.Number{
252 "-12.50e+3",
253 Json.Certified{Json.number_proof("-12.50e+3", {==})}
254 }} : Result<&1, &1, Json.Error, Json.Value> }
255
256law gpu_batch_matches_cpu:
257 for batch: Json.Batch {
258 Json.parse_batch_gpu(batch) == Json.parse_batch(batch) : Json.BatchResult
259 }
260
261# ============================================================
262# URL component encoding
263# ============================================================
264
265# Encode each UTF-8 byte with an uppercase percent escape.
266law url_component_ascii:
267 { URL.percent_component("A") == "%41" : String }
268
269law url_component_reserved:
270 { URL.percent_component("/") == "%2F" : String }
271
272law url_component_utf8:
273 { URL.percent_component(SCon{Chr{233}, SNil{}}) == "%C3%A9" : String }