كل تفاعل حلقة من حدث عودةً إلى الشاشة، والمترجم يتحقق من كل حلقة فيها.
يعمل كل برنامج Orb بحلقة واحدة:
Event → Guard → Transition → Effects → UI → Eventيصل حدث. إن كان للحالة الحالية انتقال له وشرطه متحقق، يُنفَّذ الانتقال، وتعمل تأثيراته بالترتيب، وتُعاد رسم الشاشة، وتقدّم الشاشة الجديدة الأحداث التالية. لا شيء آخر يحرّك البرنامج.
في هذا المثال يبدأ الطلب غير مدفوع. لا يُقبل PAY إلا إن كان المبلغ موجبًا، ولا يوجد SHIP من الحالة pending، فلا يمكن شحن طلب غير مدفوع. هذا ليس فحصًا تذكّر أحدهم كتابته، بل هو شكل البرنامج.
Checkout
on Order · states: 3 · transitions: 4السمة نفسها كآلة حالات: كل مربع حالة، وكل سهم حدث ينقلها، والأيقونات على السهم هي التأثيرات التي يشغّلها ذلك الحدث. مرّر المؤشر فوق أي رمز لترى ما يفعله. كيف تقرأ 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}ما الذي يحدث عندما يقع الحدث PAY:
(> @payload.amount 0)(set @entity.total @payload.amount)لأن كل حلقة معلنة، يستطيع orb validate إثبات أن الحلقة تنغلق:
?amount يجب أن يعلن amount بالنوع الصحيح.المعيار صفر أخطاء وصفر تحذيرات. التحذير اكتشاف، لا حدّ أدنى مقبول.
التحقق يثبت أن البرنامج سليم البنية، وorb verify يثبت أنه يفعل ما يقول: يشغّل كل انتقال، ويتحقق من الحالة التي يصل إليها والتأثيرات التي ينفذها والشاشة التي يرسمها، ويفشل عند العناصر التفاعلية الميتة والتغييرات التي لا تُحفظ أبدًا.
orb verify checkout.lolo
orb verify checkout.lolo --trait Checkout
orb verify checkout.lolo --allيشغّل --all الدائرة نفسها في ثلاثة محركات (نواة Rust وبيئة JavaScript والتطبيق المترجَم) فلا يمكن أن تتباعد.
يسرد مرجع التحقق الفحوص برموزها. ويعرض التركيب كيف تعيد استخدام دوائر كاملة.