Бағдарламаны жетілдіру – бұл компьютерлік бағдарламаларды түзету және қарапайымдастыру әдісі. Формалды әдістерде, бұл абстрактілі сипаттамадан нақты бағдарламаға өту процесі. Scrum-да да қолданылады.
Ағылшыншамен салыстырыңыз: абзацты басыңыз — түпнұсқа терезеде ашылады. Абзац астындағы EN түймесі оны мәтін ішінде көрсетеді.
Мазмұны
Кіріспе
Нақтылау – компьютерлік ғылымның жалпылама термині, компьютерлік бағдарламаларды дұрыс жасау және қолданыстағы бағдарламаларды формалды тексеруге қолайлы ету үшін қолданылатын әртүрлі тәсілдерді қамтиды.
Refinement is a generic term of computer science that encompasses various approaches for producing correct computer programs and simplifying existing programs to enable their formal verification.
Бағдарламаны жетілдіру
Ресми әдістерде бағдарламаны жетілдіру – абстрактілік (жоғары деңгейдегі) ресми сипаттаманы нақты (төмен деңгейдегі) орындалатын бағдарламаға тексеріле алатын түрлендіру. Кезеңдемелі жетілдіру осы процесті сатылар бойынша жүргізуге мүмкіндік береді. Логикалық тұрғыдан алғанда, жетілдіру көбінесе қынауды қамтиды, бірақ қосымша қиындықтар туындауы мүмкін. Scrum сияқты икемді бағдарламалық жасақтаманы әзірлеу тәсілдеріндегі өнімдік артта қалудың (талаптар тізімі) уақтылы және кезеңдемелі дайындалуы да жиі жетілдіру деп сипатталады.
In formal methods, program refinement is the verifiable transformation of an abstract (high level) formal specification into a concrete (low level) executable program. Stepwise refinement allows this process to be done in stages. Logically, refinement normally involves implication, but there can be additional complications. The progressive just in time preparation of the product backlog (requirements list) in agile software development approaches, such as Scrum, is also commonly described as refinement.
Деректерді жетілдіру
Деректерді жетілдіру абстрактілі дерек моделін (мысалы, жиынтар түрінде) іске асырылатын дерек құрылымдарына (мысалы, массивтерге) түрлендіру үшін қолданылады. Операцияны жетілдіру жүйедегі операцияның сипаттамасын іске асырылатын бағдарламаға (мысалы, процедураға) айналдырады. Бұл процесте постшартты күшейтуге және/немесе алғышартты әлсіретуге болады. Бұл сипаттамадағы кез келген беймәлімдікті, әдетте, толыққанды детерминистік іске асыруға дейін азайтады. Мысалы, x ∈ {1,2,3} (мұнда x – операциядан кейін x айнымалысының мәні) x ∈ {1,2}, содан кейін x ∈ {1} деп тазартылуы мүмкін және x := 1 ретінде іске асырылуы мүмкін. Бұл жағдайда x := 2 және x := 3 іске асырулары да бірдей қабылданады, тазарту үшін басқа жол қолданылады. Дегенмен, x ∈ {} (жалғанға тең) деп тазартпауға сақтану керек, өйткені мұны іске асыру мүмкін емес; бос жиыннан элемент таңдау мүмкін емес. Кейде реификация термині де қолданылады (Клифф Джонс ұсынған). Формалды тазарту мүмкін болмаған жағдайда қолданылатын балама әдіс – ретроспекция. Тазартудың қарама-қарсысы – абстракция.
Data refinement is used to convert an abstract data model (in terms of sets for example) into implementable data structures (such as arrays). Operation refinement converts a specification of an operation on a system into an implementable program (e. g., a procedure). The postcondition can be strengthened and/or the precondition weakened in this process. This reduces any nondeterminism in the specification, typically to a completely deterministic implementation. For example, x ∈ {1,2,3} (where x is the value of the variable x after an operation) could be refined to x ∈ {1,2}, then x ∈ {1}, and implemented as x := 1. Implementations of x := 2 and x := 3 would be equally acceptable in this case, using a different route for the refinement. However, we must be careful not to refine to x ∈ {} (equivalent to false) since this is unimplementable; it is impossible to select a member from the empty set. The term reification is also sometimes used (coined by Cliff Jones). Retrenchment is an alternative technique when formal refinement is not possible. The opposite of refinement is abstraction.
Тазарту калькулі
Тазарту калькулі – бағдарламаны жетілдіруге бағытталған формальды жүйе (Хоар логикасынан шабыттанған). ФермаТ трансформация жүйесі – тазартудың өнеркәсіптік деңгейдегі іске асырылуы. B әдісі – тазарту калькулісін компоненттік тілмен толықтыратын формальды әдіс; ол өнеркәсіптік жобаларда қолданылған.
Refinement calculus is a formal system (inspired from Hoare logic) that promotes program refinement. The FermaT Transformation System is an industrial strength implementation of refinement. The B Method is also a formal method that extends refinement calculus with a component language: it has been used in industrial developments.
Тазарту түрлері
Типтер теориясында, тазартылған тип – кез келген элементі үшін дұрыс деп есептелетін предикатпен жабдықталған тип. Тазартылған типтер функция аргументтері ретінде алдын-шарттарды немесе қайтарым типтері ретінде пост-шарттарды білдіре алады: мысалы, табиғи сандарды қабылдап, 5-тен үлкен табиғи сандарды қайтаратын функцияның типі осылай жазылуы мүмкін. Тазартылған типтер осылайша мінез-құлықтық субтипімен байланысты.
In type theory, a refinement type is a type endowed with a predicate which is assumed to hold for any element of the refined type. Refinement types can express preconditions when used as function arguments or postconditions when used as return types: for instance, the type of a function which accepts natural numbers and returns natural numbers greater than 5 may be written as Refinement types are thus related to behavioral subtyping.