Axiomatic definition of Loglan'82: Różnice pomiędzy wersjami
(→Declarations of variables. Assignment instructions) |
(→\mathcal{L}_{1} Declarations of variables. Assignment instructions) |
||
| Linia 78: | Linia 78: | ||
<math>\{x:=\tau\}( \alpha ) \Leftrightarrow \alpha(x/\tau)</math> | <math>\{x:=\tau\}( \alpha ) \Leftrightarrow \alpha(x/\tau)</math> | ||
| + | |||
| + | === <math>\mathcal{L}_{2}</math> Conditional instructions === | ||
| + | === <math>\mathcal{L}_{3}</math> Arrays and '''for''' instructions === | ||
| + | === <math>\mathcal{L}_{4}</math> Iteration instructions === | ||
Wersja z 16:08, 16 paź 2015
On these pages we are sketching, in an incremental way, an axiomatic semantics of Loglan'82.
Spis treści
- 1 Axiomatic definitions of sublanguages of Loglan'82
Axiomatic definitions of sublanguages of Loglan'82
Here we shall present an increasing sequence of sublanguages [math]\mathcal{L}_0\subset\mathcal{L}_1\subset\mathcal{L}_2\subset \mathcal{L}_3\subset\mathcal{L}_4\subset \dots[/math]Loglan'82. For each language [math]\mathcal{L}_i[/math] we shall present its grammar and some axioms and inference rules that define its semantics.
Program
Program in Loglan'82 has the following structure
| definiendum | definiens |
|---|---|
| program | program <name>;
begin
end |
where name is any identifier, i.e. a finite sequence of letters and digits beginning with a letter.
The declarations and instructions are finite sequences of declarations and instructions respectively, empty squence included.
This allow us to define the first sublanguage [math]\mathcal{L}_{0,0}[/math] of Loglan'82.
Language [math]\mathcal{L}_{0,0}[/math]
[math]\mathcal{L}_{0,0} \stackrel{df}{=}\{p\in \mathcal{A}^*: p=\textbf{program}\ \textit{id}; \textbf{begin end} \}[/math]
Programs of the language [math]\mathcal{L}_{0,0}[/math] are empty programs, they posses just a name. Their list of instructions as well as list of declarations are empty. The effect of execution of such program is do nothing.
Language [math]\mathcal{L}_{0,1}[/math]
Now we shall define a new language [math]\mathcal{L}_{0.1}[/math]. First, we say that any expression of the form:
writeln;
write(integer);
write("here your text");
is an output instruction.
[math]\mathcal{L}_{0.1} \stackrel{df}{=}\{p\in \mathcal{A}^*: p=\textbf{program} \textit{ id}; \textbf{begin} \lt\textit{output instructions}\gt \textbf{end} \}[/math]
| program print; begin
end |
Semantics
Each output instruction appends a string of characters to the standard output.
[math]\mathcal{L}_{1}[/math] Declarations of variables. Assignment instructions
Now we shall introduce the linear programs. Each program of this group contains declarations of variable and the instructions of a program are the assignment instructions only.
The language [math]\mathcal{L}_{1}[/math] is the closure of languages [math]\mathcal{L}_{1,c} \cup \mathcal{L}_{1,s}\cup \mathcal{L}_{1,b}\cup \mathcal{L}_{1,i}\cup \mathcal{L}_{1,r}[/math]
Language [math]\mathcal{L}_{1,c}[/math]
Declarations are declarations of variables of type char.
Example
Example
program P2 ;
- var x,y: integer;
begin
- y:=74;
- x:= y+ 8;
end
Grammar
Context free grammar
Well formed expressions
Axiom
[math]\{x:=\tau\}( \alpha ) \Leftrightarrow \alpha(x/\tau)[/math]
