Хм. А быть может подойти к дело более общо?
Что есть функция или процедура? Это есть кусок кода который что-то делает. У этого куска кода есть вход и выход. Все. Таким образом нужно явно указать что этому куску подаем на вход, и что будем принимать на выходе. Именно явно, а не как сейчас.
Допустим у нас есть штука которая модифицирует даденый массив и попутно что-то печатает в лог а также сообщает смогла или не смогла она довести работу до конца. Очевидно что для работы ей потребуется доступ к нашему массиву на чтение и запись, доступ на запись к логу, и доступ на запись к нашему возвращаемому значению. Так почему бы прямо так и не написать?
Вот предположим у нас эта гм... ну пусть процедура (далее псевдокод):
proc foo require
arr : Array of Int (read, write),
log : Logger (write),
res : Boolean (write) := False;
begin
for I in range(arr) do
arr(I) := arr(I)+1;
log.writeln(arr(I));
end
res := True;
end foo
Ну и соответственно использование:
res : Boolean;
my_log : SysLogger;
my_array : Array (1..100) of Int;
...
fooCall is foo with my_log (write), res (write), my_array (read, write);
do fooCall;
Многословно? Возможно, но это лишь псевдокод, так понятней. Синтаксис штука вторичная, можно допилить.
Важно что мы и в спецификации и при использовании ЯВНО указываем до чего может данная процедура получить доступ. И какой именно доступ. Частичная конкретизация доступа тоже возможна:
my_log : SysLogger;
fooSysLog is foo with my_log (write);
..
foo1 is fooSysLog with res1 (write), my_array1(read, write);
do foo1;
foo2 is fooSysLog with res2 (write), my_array1(read, write);
do foo2;