The Alma Project, or How First-Order Logic Can Help Us in Imperative Programming - Correct System Design: Recent Insights and Advances - page 92

3.2 Job Shop Scheduling

The second problem we discuss is a classical scheduling problem, namely the job
shop scheduling problem. We refer to [5, page 242] for its precise description.
Roughly speaking, the problem consists of scheduling over time a set of jobs,
each consisting of a set of consecutive tasks, on a set of processors.
The input data is represented by an array of jobs, each element of which is
a record that stores the number of the tasks and the array of tasks. In turn,
each task is represented by the machine it uses and by its length. The output is
delivered as an integer matrix that (like a so-called Gantt chart) for each time
point k and each processor p stores the job number that p is serving at the time

k

point .

The constraint that each processor can perform only one job at a time is
enforced by using generalized equality on the elements of the output matrix.
More precisely, whenever job i requires processor j for a given time window

[ d 1 ;d 2 ], the program attempts for some k to initialize the elements of the matrix

( . If this initialization

succeeds, the program continues with the next task. Otherwise some element in
this segment is already initialized, i.e., in this segment processor

j; k + d 1 ) ; ( j; k + d 1 +1) ;:::; ( j; k + d 2 ) to the value i

is already
used by another job. In this case the execution fails and through backtracking
the next value for

j

is chosen.
The constraint that the tasks of the same job must be executed in the pro-
vided order and cannot overlap in time is enforced by the use of the variable
min start time which, for each job, initially equals 1 and then is set to the end
time of the last considered task of the job. To perform this update we exploit
the fact that when the SOME statement is exited its index variable k equals the
smallest value in the considered range for which the computation does not fail
(as explained in [2]).
We provide here the procedure that performs the scheduling. For the sake of
brevity the rest of the program is omitted.

k

TYPE
TaskType = RECORD

machine : INTEGER;
length : INTEGER;

END;

JobType = RECORD

tasks : INTEGER;
task : ARRAY [1..MAX_TASKS] OF TaskType

END;
JobVectorType = ARRAY [1..MAX_JOBS] OF JobType;
GanttType = ARRAY [1..MAX_MACHINES],[1..MAX_DEADLINE] OF INTEGER;

PROCEDURE JobShopScheduling(VAR job: JobVectorType; deadline:INTEGER;
jobs :INTEGER; VAR gantt: GanttType);

VAR
i, j, k, h : INTEGER;
min_start_time : INTEGER;