stack : CONTEXT = BEGIN optype: TYPE = {pop, push, noop}; Data: TYPE; c0: ARRAY NATURAL OF Data; trash : Data; S: MODULE = BEGIN INPUT op : optype INPUT data : Data LOCAL contents : ARRAY NATURAL OF Data LOCAL top : NATURAL OUTPUT first : Data OUTPUT invalid_pop : BOOLEAN DEFINITION first = IF top > 0 THEN contents[top-1] ELSE trash ENDIF; %% return "trash" since the stack is empty invalid_pop = (op = pop AND top = 0) %% invalid_pop signs an invalid use of S INITIALIZATION top = 0; contents = c0 TRANSITION top' = IF op = push THEN top + 1 ELSIF op = pop AND top > 0 THEN top - 1 ELSE top ENDIF; contents' = IF op = push THEN (contents WITH [top] := data) %% update the top of the stack ELSE contents ENDIF END; %% %% %% Test scenario %% %% d0: Data; d1: Data; d2: Data; dummy: Data; num_steps: NATURAL = 6; %% sequence of operations to be executed op_seq : ARRAY NATURAL OF optype = [ [i : NATURAL] IF i <= 2 THEN push %% three pushes ELSIF i <= 5 THEN pop %% followed by three pops ELSE noop ENDIF ]; %% send noop (no operation) %% sequence of data to send data_seq : ARRAY NATURAL OF Data = [ [i : NATURAL] IF i = 0 THEN d0 %% send d0 in the first step ELSIF i = 1 THEN d1 %% send d1 in the second step ELSIF i = 2 THEN d2 %% send d2 in the third step ELSE dummy ENDIF]; %% otherwise send dummy test_bench1: MODULE = BEGIN OUTPUT op : optype OUTPUT data : Data INPUT first : Data LOCAL step : NATURAL LOCAL first_seq : ARRAY NATURAL OF Data DEFINITION data = data_seq[step]; %% data to send in the current step op = op_seq[step] %% op to execute in the current step INITIALIZATION step = 0; first_seq[0] = first %% record the top of the stack in the initial step TRANSITION step' = step + 1; first_seq'[step'] = first' %% record the top of the stack in the next step END; system1: MODULE = (S || test_bench1); th1: THEOREM system1 |- G(step >= (num_steps - 1) => (first_seq[3] = d2 AND first_seq[4] = d1 AND first_seq[5] = d0)); th2: THEOREM system1 |- G(NOT invalid_pop); invalid: THEOREM system1 |- G(step >= (num_steps - 1) => (first_seq[3] = d0 AND first_seq[4] = d1 AND first_seq[5] = d2)); END