|
|
|---|
|
|
|
|---|
Static checks on Leo programs and inputs.
In order to execute and compile Leo, the static semantics requirements must hold on both the program and the input file. These requirements include not only the individual ones on the program and the input file, but also a consistency requirement between program and input file, namely that the function parameters obtained from the input file match the ones of the main function. The matching is modulo permutation, because an input file may list its sections and items in any order.