Zaprti krog
Vsaka interakcija je zanka od dogodka nazaj do zaslona, prevajalnik pa preveri vsak njen rob.
Vsak program Orb teče v eni zanki:
Event → Guard → Transition → Effects → UI → EventPrispe dogodek. Če ima trenutno stanje zanj prehod in njegov pogoj drži, se prehod izvede, učinki se izvedejo po vrsti, zaslon se znova nariše, nov zaslon pa ponudi naslednje dogodke. Nič drugega programa ne premakne.
En korak
V tej blagajni naročilo začne neplačano. PAY je sprejet le, če je znesek pozitiven; iz pending ni SHIP, zato neplačano naročilo ne more na pot. To ni preverjanje, ki se ga je nekdo spomnil napisati; to je oblika programa.
Checkout
on Order · states: 3 · transitions: 4Unpaid
Ista lastnost kot avtomat stanj: vsak okvir je stanje, vsaka puščica dogodek, ki ga premakne, ikone na puščici pa so učinki, ki jih ta dogodek izvede. Z miško pojdite čez simbol in videli boste, kaj naredi. Kako brati AVL
1app std-orb-sample-checkout "1.0.0"
2"std-orb-sample-checkout — the checkout program shown on orb.almadar.io's home page, running: an order that cannot ship before it is paid. The page shows this file as code beside the running trait, and each move is reported (MOVED) so its state machine can follow along."
3orbital Orders {
4 entity Order [runtime] {
5 id : string!
6 total : number
7 }
8
9 trait Checkout -> Order [interaction, instance] {
10 initial: pending
11
12 state pending {
13 INIT -> pending
14 (render-ui main { type: stack, gap: sm, children: [
15 { type: typography, content: "Unpaid", variant: h4 },
16 { type: button, label: "Pay 40", action: PAY, actionPayload: { amount: 40 } }
17 ] })
18 PAY -> paid when (> ?amount 0)
19 (set @entity.total ?amount)
20 (emit MOVED { event: "PAY" })
21 (render-ui main { type: stack, gap: sm, children: [
22 { type: typography, content: "Paid 40", variant: h4 },
23 { type: button, label: "Ship", action: SHIP }
24 ] })
25 }
26
27 state paid {
28 SHIP -> shipped
29 (emit MOVED { event: "SHIP" })
30 (render-ui main { type: stack, gap: sm, children: [
31 { type: typography, content: "Shipped", variant: h4 },
32 { type: button, label: "New order", action: NEW_ORDER }
33 ] })
34 }
35
36 state shipped {
37 NEW_ORDER -> pending
38 (emit MOVED { event: "NEW_ORDER" })
39 (render-ui main { type: stack, gap: sm, children: [
40 { type: typography, content: "Unpaid", variant: h4 },
41 { type: button, label: "Pay 40", action: PAY, actionPayload: { amount: 40 } }
42 ] })
43 }
44
45 emits {
46 PAY {
47 amount : number!
48 }
49 MOVED -> external {
50 event : string!
51 }
52 @description "Each move names the event it took, so a diagram beside the order can follow it."
53 }
54 }
55
56 page "/checkout" -> Checkout
57}Kaj se zgodi, ko se sproži PAY:
→
paid(> @payload.amount 0)(set @entity.total @payload.amount)Kaj preveri prevajalnik
Ker je vsak rob naveden, lahko orb validate dokaže, da se zanka sklene:
- Vsak element nekam vodi. Gumb, katerega dogodka ne sprejme nobeno stanje, je napaka.
- Vsako stanje je mogoče zapustiti, razen če naj bo konec, in vsako stanje je dosegljivo.
- Vsak oddan dogodek je slišan. Zunanji dogodek brez poslušalca je sporočen.
- Vsaka plast se izprazni. Modalno okno, odprto v stanju, mora biti zaprto na vsakem izhodu iz njega.
- Vsaka stran nekaj prikaže in vsaka je dosegljiva.
- Tovori se ujemajo. Dogodek, prebran kot
?amount, mora navestiamount, s pravim tipom.
Merilo je 0 napak in 0 opozoril. Opozorilo je ugotovitev, ne spodnja meja.
Nato testiraj
Preverjanje dokaže, da je program pravilno zgrajen. orb verify dokaže, da naredi, kar pravi: izvede vsak prehod, preveri stanje, v katerem pristane, učinke in zaslon ter pade pri mrtvih elementih in spremembah, ki se nikoli ne shranijo.
orb verify checkout.lolo
orb verify checkout.lolo --trait Checkout
orb verify checkout.lolo --all--all izvede isti krog v treh pogonih (jedro v Rustu, okolje JavaScript in prevedena aplikacija), da se ne morejo razhajati.
Naprej
Referenca preverjanja našteje preverjanja po kodah. Sestavljanje pokaže, kako ponovno uporabiš cele kroge.