Flow chart language

Syntax

We specify the syntax of Janus using Backus–Naur form.

An FCL program is a list of formal parameter declarations, an entry label, and a sequence of basic blocks:

Initially, the language only allows non-negative integer variables.

A basic block consists of a label, a list of assignments, and a jump.

An assignment assigns a variable to an expression. An expression is either a constant, a variable, or application of a built-in n-ary operator:

Note, variable names occurring throughout the program need not be declared at the top of the program. The variables declared at the top of the program designate arguments to the program.

As values can only be non-negative integers, so can constants. The list of operations in general is irrelevant, so long as they have no side effects, which includes exceptions, e.g. division by 0:

Where =, <, ... have semantics as in C. The semantics of - is such that if x-y<0, then x-y=0.

Example

We write a program that computes the n^th Fibonacci number, for n>2:

(n)(init)init: x1 = 1 x2 = 1fib: x1 = x1 + x2 t = x1 x1 = x2 x2 = t n = -(n 1) if >(n 2) then fib else exitexit: return x2

Where the loop invariant of fib is that x1 is the (i+2-1)^th and x2 is the (i+2)^th Fibonacci number, where i is the number of times fib has been jumped to.

We can check the correctness of the method for n=4 by presenting the execution trace of the program:

( i n i t ,   [ n ↦ 4 ,   x 1 ↦ 0 ,   x 2 ↦ 0 ,   t ↦ 0 ] ) → ( f i b ,   [ n ↦ 4 ,   x 1 ↦ 1 ,   x 2 ↦ 1 ,   t ↦ 0 ] ) → ( f i b ,   [ n ↦ 3 ,   x 1 ↦ 1 ,   x 2 ↦ 2 ,   t ↦ 0 ] ) → ( ⟨ h a l t ,   3 ⟩ ,   [ n ↦ 2 ,   x 1 ↦ 2 ,   x 2 ↦ 3 ,   t ↦ 0 ] )

Where ⟨ h a l t ,   v ⟩ marks a final state of the program, with the return value v .