MODULE ms;
IMPORT StdLog, seq;
(*
MODULE seq;
VAR
oes*, open: BOOLEAN;
len, pos: LONGINT;
(* ~undefined(open) & ~undefined(len) & (0 <= len) & (len < MAX(LONGINT)) *)
(* open <= ~undefined(oes) & ~undefined(pos) & (1 <= pos) & (pos <= len + 1) & (oes = (pos = len + 1)) *)
(* ~open <= undefined(oes) & undefined(pos) *)
(* open' & (0 <= i') & (i' <= len') *)
PROCEDURE element (i: LONGINT): BYTE;
(* (len = len') & open & (pos = pos') & (Result = (element number i')) *)
(* ~open' *)
PROCEDURE reset*;
(* (len = len') & open & (pos = 1) *)
(* open' *)
PROCEDURE close*;
(* (len = len') & ~open *)
(* open' & ~oes' *)
PROCEDURE read* (OUT a: BYTE);
(* (len = len') & open & (pos = pos' + 1) & ~undefined(a) & (a = element(pos')) & ((a = 0) OR (a = 1)) *)
BEGIN
END seq.
*)
VAR
a: BYTE;
i: INTEGER;
(* seq.open' & ~undefined(i') & (i' = seq.pos' - 2) & (def: element(0) = 1) & ~undefined(a') & (a' = element(i' + 1)) *)
PROCEDURE p* (VAR a, i: INTEGER);
VAR b: BOOLEAN;
BEGIN
b := FALSE;
WHILE ((a # 0) OR ~b) & ~seq.oes & (i < MAX(INTEGER)) DO
b := (a = 0);
seq.read(a);
INC(i)
END;
IF (a = 0) & b THEN
StdLog.Int(i);
StdLog.Ln
ELSIF seq.oes THEN
StdLog.Bool(FALSE);
StdLog.Ln
ELSE
StdLog.String('limit length');
StdLog.Ln
END
END
(* (seq.len = seq.len') & seq.open & (def: element(0) = 1) & ~undefined(i) *)
(* i = min({j | j IN {i' .. MIN(seq.len, MAX(INTEGER)) - 1}: (element(j) = 0) & (element(j + 1) = 0)} + {MIN(seq.len, MAX(INTEGER))}) *)
(* (seq.pos = i + 2) & ~(a) & (a = element(i + 1)) *)
BEGIN
seq.reset; (* seq.open *)
a := 1; (* a = element(0) *)
i := -1; (* i = seq.pos - 2 *)
p(a, i); (* p(a, i); p(a, i); p(a, i); ... *)
seq.close (* ~seq.open *)
END ms.Сам алгоритм:
a := 1;
b := FALSE;
i := -1;
WHILE ((a # 0) OR ~b) & ~seq.oes & (i < MAX(INTEGER)) DO
b := (a = 0);
seq.read(a);
INC(i)
END;
IF (a = 0) & b THEN
StdLog.Int(i);
StdLog.Ln
ELSIF seq.oes THEN
StdLog.Bool(FALSE);
StdLog.Ln
ELSE
StdLog.String('limit length');
StdLog.Ln
END
