Basic statement is assignment, control structures are 'if' and 'while':

x = T
if (F) c1 else c2
c1 ; c2
while (F) c1

We can describe the syntax of this language using a Context-Free Grammar:

 c ::=  x=T | (if (F) c else c) | c ; c | (while (F) c)
 T ::= K | V | (T + T) | (T - T) | (K * T) | (T / K) | (T % K)
 F ::= (T=T) | (T < T) | (T > T) | (~F) | (F & F) | (F|F)
 V ::= x | y | z | ...
 K ::= 0 | 1 | 2 | ...

This specifies our language as a set of strings.

More abstractly, we can represent it as syntax tree, using abstract syntax trees, which are more appropriate for analysis, compilation, and proofs. In abstract syntax we do not need to worry about parentheses, keywords etc.

Each program has a finite number of integer variables.

The meaning is what you would expect from the corresponding subset of Java, but integers are true mathematical integers.

Example program:

while (x > 1) {
  if (x % 2 = 0) 
    x = x / 2
  else 
    x = 3 * x + 1
}

Does this program terminate for all positive integers? (Collatz conjecture)

This language is Turing-complete

• it subsumes counter machines, which are known to be Turing-complete
• every possible program (Turing machine) can be somehow encoded into computation into integers (not always in a natural way: computed integers can become very large)
• the problem of taking a program and checking whether it terminates is undecidable
• Rice's theorem: all properties of programs that are expressed in terms of the results that the programs compute (and not in terms of the structure of programs) are undecidable

Note: in real programming languages we have bounded integers, but we have other sources of unboundedness

• example: sizes of linked lists and other containers
• bignums
• program syntax trees for an interpreter or compiler (would like to handle programs of any size)