Допускается ли одновременный доступ?
Заключительное замечание относится к одному из важных свойств предложенного подхода - требованию, чтобы в каждый момент времени не более чем один клиент мог иметь доступ к каждому объекту-поставщику. Для VIP-клиентов предоставляется механизм дуэлей.
Причина запрета понятна: если бы некоторый клиент мог бы прервать в любой момент выполнение программы, запущенной его претендентом, то была бы потеряна возможность рассуждать о классах (используя свойства вида {INV and pre} body {INV and post}), поскольку прерванный претендент мог бы оставить объект в произвольном состоянии.
Такой недостаток исчез бы, если бы мы разрешили претендентам выполнять только программы весьма специального вида: аппликативные программы (в определенном в предыдущих лекциях для функций смысле), которые либо вовсе не изменяют объект, либо, изменяя его, устраняют все свои изменения перед тем, как его покинуть. Для этого нужен языковой механизм, позволяющий утверждать, что некоторая программа аппликативна, и компиляторы, обеспечивающие это свойство.
