UNITY Program Structure 7: Initially section
syntax rovnaká ako assign_section, namiesto kazdého symbolu := je všade iba =
definuje iniciálne hodnoty premenných
premenné sa vyskytujú na lavej strane najviac raz
existuje usporiadanie rovností také, ze kazdá premenná v kvantifikácii je bud viazaná alebo sa nachádza na lavej strane nejakej predchádzajúcej rovnosti
existuje usporiadanie za quantified equations, ze kazdá premenná na pravej strane alebo v indexe sa nachádza na lavej strane nejakej predchádzajúcej rovnosti
tieto dve podmienky hovoria, ze iniciálne hodnoty sú dobre definované
initially_section definuje inicial condition; je to najsilnejší predikát, ktorý platí na zaciatku
získa sa nahradením a || za ? a podmienené výrazy tvaru x = e0 if b0 ~ ... ~ en if bn výrazom
(b0 ? (x = e0)) ? ... ? (bn ? (x = en))
tento nie je ekvivalentný s
((x = e0) ? b0) ? … ? ((x = en) ? bn)
- napr. y = 2 if false