Специфична форма и състав; EWST Превод
Коректност в композиционните модели
Целта на композиционния дизайн е да може да се изгради система от компоненти. До известна степен всички чертежи са композиционни: системите са изградени от машинни декларации, които могат да се разглеждат като малки компоненти. Разбира се, за да бъде композицията полезна, ни трябва нещо повече от композиционен дизайн. Компонентът трябва да е част от проекта, т.е. той трябва да е резултат от интелектуални усилия. Само тогава композицията е полезна, което позволява на дизайнерите да споделят това интелектуално усилие.
Композитните дизайни включват различни видове проблеми. Тук се интересуваме повече от проблема за коректността: Как можем да претендираме за коректността на дадена система от спецификациите на нейните компоненти или, с други думи, какво трябва да знаем за компонентите, за да предскажем поведението на системата? Доказателството за състав наричаме доказателство за коректност, ако правилността на системата се извежда от спецификациите на компонентите. Отново, всяко доказателство за коректност в известен смисъл е доказателство за състава: ние винаги използваме определени познания за компонентите, за да докажем система. Както преди, добавяме още едно ограничение: Искаме компонентите да съдържат част от доказателството за коректност, тъй като те трябва да съдържат част от дизайна. С други думи, ние искаме да изградим доказателства за състава от изявленията, вече демонстрирани на ниво компонент, без да се налага да повтаряме някое от тези доказателства. Това изображение описва спецификациите и доказателствата в композиционен дизайн:
Интуитивно, размерът на усилието на пробата в композиционните проби ще зависи от това как са посочени компонентите. Ако спецификацията на компонент е само официално описание на изпълнението (т.е. текстът на самата програма, с добре дефинирана семантика), като например програма UNITY или CSP процес, не се извършва част от тестовите усилия на ниво компонент. и дизайнерите трябва да се занимават с оперативно и изрично описание на поведението на компонентите при конструиране на доказателство за състав. Спецификациите на компонентите трябва да са абстракции от поведението на компонентите. Те трябва да описват полезни факти за даден компонент, факти, които трябва да бъдат демонстрирани в текста на компонента. След това тези факти се използват като доказателство за състава, без задължението да бъдат доказани отново.
Всъщност разделянето на тестовите усилия не изисква композиционен дизайн. Напълно възможно е да се разделят усилията за монолитно доказателство. В този случай тя се основава на пълна спецификация на системата и оперативно описание на цялостната система и се извежда обща тежест на доказване. Тази тежест на доказване сама по себе си е разбита и доказателството за коректност е изградено от дърво и междинни резултати. Този подход е изследван, например, от Лесли Лампорт с доказателства за TLA +.
Трудността на такъв подход е, че спецификациите не могат да бъдат съставени много добре. Възможно е никакви (нетривиални) системни свойства да бъдат логически изведени от свойствата на компонентите. За работния подход спецификациите на компонентите трябва да позволяват на дизайнерите да извеждат свойствата на системата. Някои спецификации на компонентите, тъй като не съдържат достатъчно информация, не позволяват това приспадане. Проблемът е, че тъй като искаме те да бъдат абстрактни, спецификациите на компонентите може да не съдържат достатъчно информация. Очевидно има компромис между запазването на абстрактните спецификации и превръщането им в доказателство за състава: твърде много информация, твърде много подробности, открити в спецификациите, и абстракцията се губи; не е достатъчно и композицията се губи.
Случаят неизменно и винаги
За да илюстрирате баланса между абстракцията и способността за композиране, разгледайте случая на системи (и компоненти), дефинирани от безкрайното им изчисление (реактивни системи), съставени от паралелен състав. За тези системи често се използват два тясно свързани типа свойства:
- инвариант: казва се, че предикатът на състоянието е неизменен, ако:
- той поддържа в първоначално състояние всяко изчисление и
- нейната истина се запазва от всяко твърдение на системата.
- винаги: казва се, че предикатът на състоянието е „винаги вярно“, ако е вярно при всяко състояние на изчисление на системата.
В света на временната логика свойствата винаги се наричат "инварианти", докато инвариантните свойства се наричат "индуктивни инварианти". От друга страна, в света на последователната проверка на програмата, инвариантните свойства се наричат „инварианти“ и свойствата често нямат име. (Обаче те се наричат „твърдения“ в метод Б). Това доведе до известно объркване (вижте страницата за аксиома на заместването).
Естествено, винаги и неизменно са свързани: всеки предикат, който е неизменен, също винаги е верен (чрез индукция). Предикатът обаче винаги може да бъде истина и не може да бъде неизменен. Това означава, че свойствата винаги са по-слаби като цяло от инвариантните свойства. Те са и по-абстрактни: те заявяват, че предикатът е верен при всяко състояние на изчисление, но не казват защо. Неизменните свойства казват защо. С други думи, инвариантните свойства са полезен инструмент за винаги доказване на свойства, но те не са достатъчно абстрактни, за да се използват за задаване на компоненти.
По отношение на състава свойствата са неизменни и винаги се различават. Тъй като програмните изрази се запазват чрез паралелен състав, предикатът на състоянието е инвариант в системата веднага щом е инвариант във всички компоненти на системата (в нашия речник инвариантните свойства се считат за универсални). Тъй като конкурентната система може да има по-достъпни състояния от нейните компоненти, това не винаги важи за свойствата: предикатът винаги може да бъде верен във всички компоненти на системата и фалшифициран от глобално конкурентната система.
За да обобщим, инвариантните свойства могат да се комбинират, но те са твърде силни (недостатъчно абстрактни), за да се използват в спецификациите на компонентите; свойствата всъщност винаги са необходимата абстракция, но те не могат да бъдат съставени. (Полезен въпрос е да се определи кои свойства са по-слаби от инвариантните свойства, по-силни от всякога и кои все още могат да бъдат съставени.) Този въпрос не е толкова прост, колкото изглежда, че читателите са поканени да се опитат да решат провокативен въпрос, свързан с този проблем.)
Нашите изследвания
В нашето проучване Мани Чанди и аз разгледахме следния проблем: можем ли да намерим свойства на компонентите, достатъчно силни, за да бъдат съставени, но достатъчно слаби, за да запазят абстракцията? По-конкретно, ние се фокусираме върху две форми на композиция: екзистенциална (екзистенциално свойство, задържано в системата веднага щом е в поне един компонент) и универсално (универсално свойство, задържано в дадена система, щом е във всички компоненти). Ние разглеждаме тези две форми на композиция в общ контекст. Компонентите са абстрактни обекти, не непременно програми. Той не трябва да има атрибути като "състояния" или "изчисления". Те са съставени от закон за композицията, който не би трябвало да бъде паралелен състав (по-специално, не трябва да бъде симетричен или идемпотентен).
Интересни резултати (и още по-интересни въпроси) могат да бъдат изследвани в тези хипотези. Тази рамка може да се приложи към реактивни системи и времева логика; по-специално, случаят с инвариантите, разгледан по-горе, може да бъде добре изразен. Тези идеи могат да бъдат обобщени и когато се използват няколко закона за композицията заедно.