UNITY Program Structure 6: Assign section
assign_section ? statement_list
statement_list ? statement { statement }
statement ? assign_stat | quantified_statement_list
quantified_statement_list ? ? quant statement_list?
(obdlznicek): separátor medzi statements, nedeterministický výber
tiez pozadujeme, aby pocet „prípadov“ bol konecný
Obmedzenie: bool_expr v quant nesmie obsahovat premenné, ktorých hodnota sa môze zmenit pocas behu programu
Toto obmedzenie zarucuje, ze mnozina statements je pevná ? statements sa netvoria pocas výpoctu
Príklady: Priradenie jednotkovej matice do U[0..N, 0..N]
- (N + 1)2 statements:
? j, k: 0 ? j ? N ? 0 ? k ? N :: U[j, k] := 0 if j ? k ~ 1 if j = k?
- (N + 2)2 statements:
? || j, k: 0 ? j ? N ? 0 ? k ? N ? j ? k :: U[j, k] := 0 ? ? ? || j: 0 ? j ? N :: U[j, j] := 1 ?
- N + 1 statement_lists, kazdý z nich má 2 statements
? j: 0 ? j ? N :: U[j, j] := 1 ? || k: 0 ? k ? N ? j ? k :: U[j, k] := 0 ??