Семантика на езиците за програмиране 2005/06 - упражнения

Коректност на програми

• блок-схема - алгоритъм, зададен с графична схема с цел абстрахиране от езика за програмиране
• входно условие A - условие, на което трява да отговарят входните данни на дадена блок-схема
• изходно условие C - зависимостта между входни и изходни параметри, която трябва да е изпълнена при завършване на програмата
• частична коректност относно A и C - всеки път, когато входните данни изпълняват A и програмата завършва с някакъв изход, входните и изходните данни са в зависимост C
• тоталност относно A - всеки път, когато входните данни изпълняват A, програмата завършва
• тотална коректност относно A и C - всеки път, когато входните данни изпълняват A, програмата завършва и изходните и входните данни са в зависимост C
• частична коректност + тоталност = тотална коректност

Инварианта

• инварианта на цикъл - условие, свързващо входни и изходни данни и временните променливи, което е вярно всеки път, когато изпълнението на програмата попадне в началото на цикъла
• едно условие B е инварианта на програмата, ако
  1. A => B при първото влизане в цикъла
  2. B & P => B' при завъртане на цикъла, където B' е условието с новите стойности на променените в цикъла променливи, а P е условието програмата да остане в цикъл
  3. B & !P => C при излизане от цикъла, където !P е условието програмата да излезе от цикъла
• ако намерим инварианта на програмата, то сме доказали частичната й коректност относно A и C
• Как се търси инварианта?
  1. С хитра идея ;-)
  2. Заменяме някоя констана в C с променлива, така че да е изпълнено условието 3. по-горе
  3. Отслабване на условието C чрез премахване на някое от условията, съставящи C, така че да е изпълнено условието 3. по-горе
  4. Разписваме стойностите на променливите при изпълнение на програмата и търсим някоя очевидна зависимост между тях

Тоталност

• За доказателство на тоталност няма общ метод
• Ако условието е от вида i = y - намираме зависимост между стъпката на цикъла и стойността на i. Доказваме, че тя все някога ще достигне y.
• Ако условието е от вида f(i,x,y,...) > 0 - допускаме, че програмата не завършва при условие A, тогава получаваме безкрайна редица от променливи, за които е вярно f(i,x,y,...) > 0. Доказваме, че всички те са естествени числа и че редицата е намаляваща. Това е търсеното противоречие.
• Горният случай може да се обобщи, ако работим с произволно фундирано множество - в него също не може да има безкрайно намаляваща редица.

Задачи

• Блок-схеми с един цикъл можете да намерите в §1.2 на ръководството
• В някои задачи сами трябва да се сетите са входното и изходното условие. То трябва да е внимателно подбрано за да се реши лесно задачата
• стр. 17 / задача 1 (умножение) - инвариантата се намира, като заместим в C константата x с променливата i.
• стр. 18 / задача 2 (целочислено деление) - инвариантата се намира с отслабване на C - премахва се условието r < y. Тоталност - с намаляващата редица r - y.
• стр. 19 / задача 3 (факториел) - инвариантата се намира със заместване на костанта с променлива. Тоталност - за първата прогпама със стъпките на цикъла, за втората - с намаляваща редица.
• стр. 20 / задача 4 (целочислен корен) - условието C трябва да се запише много прецизно. Инвариантата се намира с отслабване на C. Тоталност - с намаляваща редица.