Специфична форма и состав; EWSTпреведи
Точност во композициските модели
Целта на композицискиот дизајн е да може да се изгради систем од компоненти. До одреден степен, сите цртежи се композициони: системите се изградени од машински декларации, што може да се види како ситни компоненти. Се разбира, за композицијата да биде корисна, ни треба нешто повеќе од композицискиот дизајн. Компонента мора да биде дел од проектот, односно мора да произлегува од интелектуален напор. Само тогаш композицијата е корисна, дозволувајќи им на дизајнерите да го споделат овој интелектуален напор.
Композитните дизајни вклучуваат различни видови проблеми. Тука повеќе нè интересира проблемот со исправноста: Како можеме да тврдиме за точноста на системот од спецификациите на неговите компоненти или, со други зборови, што треба да знаеме за компонентите за да го предвидиме однесувањето на системот? Доказот за составот го нарекуваме доказ за исправност ако точноста на системот се изведе од спецификациите на компонентите. Повторно, секој доказ за исправност е, во извесна смисла, доказ за составот: ние секогаш користиме одредено знаење за компонентите за да докажеме систем. Како и претходно, додаваме уште едно ограничување: Сакаме компонентите да содржат некои докази за исправност, бидејќи тие треба да содржат дел од дизајнот. Со други зборови, ние сакаме да изградиме докази за составот од искажаните изјави на ниво на компонента, без да мора да повторуваме ниту еден од овие докази. Оваа слика ги опишува спецификациите и доказите во композицискиот дизајн:
Интуитивно, количината на напор за примерок во примероците од составот ќе зависи од тоа како се специфицирани компонентите. Ако спецификацијата на компонентата е само официјален опис на спроведувањето (т.е. самиот текст на програмата, со добро дефинирана семантика), како што е програмата на УНИТЕТ или процес на ССП, ниту еден дел од тест-напорот не се изведува на компонентата на ниво. а дизајнерите мора да се занимаваат со оперативен и експлицитен опис на однесувањето на компонентите при конструирање доказ за составот. Спецификациите на компонентите мора да бидат апстракции на однесувањето на компонентите. Тие мора да опишат корисни факти за компонента, факти кои мора да бидат демонстрирани во текстот на компонентата. Овие факти потоа се користат во доказ за составот, без обврска повторно да се докажат.
Всушност, поделбата на напорот за тестирање не бара композициски дизајн. Совршено е можно да се подели напорот да се направи монолитен доказ. Во овој случај, тој се заснова на комплетна спецификација на системот и оперативен опис на комплетниот систем и се прави целосен товар на докажување. Овој товар на докажување е сам распаднат, а доказот за исправност е изграден од дрво и средни резултати. Овој пристап беше испитан, на пример, од Лесли Лампорт со примероци од TLA +.
Тешкотијата на ваквиот пристап е што спецификациите не можат да се состават многу добро. Можно е ниедно (нетривијално) својство на системот логично да се заклучи од својствата на компонентата. За работниот пристап, спецификациите на компонентите мора да им овозможат на дизајнерите да заклучат својства на системот. Некои спецификации на компонентите, бидејќи не содржат доволно информации, не го дозволуваат ова намалување. Проблемот е во тоа што бидејќи ние сакаме да бидат апстрактни, спецификациите на компонентите можеби немаат доволно информации. Постои јасно компромис помеѓу чувањето на апстрактните спецификации и нивното претворање во доказ за составот: премногу информации, премногу детали што се наоѓаат во спецификациите и апстракцијата се губат; тоа не е доволно и составот е изгубен.
Случајот секогаш и секогаш
За да ја илустрираме рамнотежата помеѓу апстракцијата и можноста за компонирање, разгледај го случајот на системи (и компоненти) дефинирани со нивната бесконечна пресметка (реактивни системи), составени од паралелен состав. За овие системи, често се користат два тесно поврзани типа на својства:
- непроменлива: се вели дека предикатот на државата е непроменлив ако:
- ја задржува во почетната состојба секоја пресметка и
- неговата вистина е зачувана со каква било изјава на системот.
- секогаш: се вели дека предикатот на состојбата е „секогаш вистинит“ ако е точно во која било состојба на пресметка на системот.
Во светот на временската логика, својствата секогаш се нарекуваат „инваријанти“, додека непроменливите својства се нарекуваат „индуктивни инваријанти“. Од друга страна, во светот на секвенцијална проверка на програмата, непроменливите својства се нарекуваат „непроменливи“ и својствата секогаш често немаат име. (Сепак, тие се нарекуваат „изјави“ во методот Б). Ова доведе до одредена конфузија (видете ја страницата за аксиома за замена).
Природно, секогаш и секогаш се поврзани: секој предикат што е непроменлив, исто така е секогаш вистинит (со индукција). Сепак, предикатот секогаш може да биде вистинит и не може да биде непроменлив. Ова значи дека својствата се секогаш воопшто послаби од непроменливите својства. Тие се исто така поапстрактни: тие наведуваат дека предикатот е точен во каква било состојба на пресметка, но тие не кажуваат зошто. Непроменливите својства кажуваат зошто. Со други зборови, непроменливите својства се корисна алатка за секогаш докажување на својствата, но тие не се доволно апстрактни за да се користат за специфицирање на компонентите.
Во однос на составот, својствата се непроменливи и секогаш се разликуваат. Бидејќи програмските искази се зачувани со паралелен состав, состојбата на предикатот е непроменлива во системот штом е непроменлива во сите компоненти на системот (во нашиот вокабулар, непроменливите својства се сметаат за универзални). Бидејќи конкурентскиот систем може да има подостапни состојби од неговите компоненти, тоа не е секогаш случај за својствата: предикатот секогаш може да биде точен во сите компоненти на системот и фалсификуван од глобално конкурентскиот систем.
Да резимираме, непроменливите својства можат да бидат сложени, но тие се премногу силни (не се доволно апстрактни) за да се користат во спецификациите на компонентите; својствата се секогаш всушност неопходна апстракција, но тие не можат да се состават. (Корисно прашање е да се утврди кои својства се послаби од непроменливите својства, посилни од кога било, и кои сè уште можат да бидат составени.) Ова прашање не е толку едноставно како што се чини дека читателите се поканети да се обидат да го решат провокативно прашање поврзано со овој проблем.)
Нашите истражувања
Во нашата студија, Мани Ченди и јас се справивме со следниот проблем: дали можеме да најдеме својства на компоненти доволно силни за да бидат составени, но доволно слаби за да ја задржат апстракцијата? Поточно, ние се фокусираме на две форми на состав: егзистенцијална (егзистенцијална особина што се чува во системот веднаш штом е во барем една компонента) и универзална (универзална својство што се чува во систем веднаш штом е во сите компоненти). Ние ги разгледуваме овие две форми на состав во општ контекст. Компонентите се апстрактни ентитети, не мора програми. Не смее да има атрибути како што се „состојби“ или „пресметки“. Тие се составени од закон за композиција за кој не се претпоставува дека е паралелен состав (особено не треба да биде симетричен или идемпотентен).
Интересни резултати (па дури и поинтересни прашања) може да се истражат во овие хипотези. Оваа рамка може да се примени на реактивните системи и временската логика; особено, случајот на инваријанти, дискутиран погоре, може да биде убаво изразен. Овие идеи можат да се генерализираат и кога се користат неколку закони на состав.