Ағылшыншамен салыстырыңыз: абзацты басыңыз — түпнұсқа терезеде ашылады. Абзац астындағы EN түймесі оны мәтін ішінде көрсетеді.
Мазмұны
Кіріспе
Guarded Command Language (GCL) - Эдсгер Дайкстраның EWD472 еңбегінде предикат түрлендіргіш семантикасы үшін анықтаған бағдарламалау тілі. Ол бағдарламалау ұғымдарын ықшам түрде үйлестіреді. Бұл бағдарламаны және оның дұрыстығын бірдей дамытуды жеңілдетеді, мұнда дұрыстық идеялары бағыт береді; сонымен қатар, бағдарламаның бөліктерін есептеп табуға болады. GCL-дің маңызды қасиеті – бұл беймәлімдік. Мысалы, егер операторында бірнеше шарттар орындалуы мүмкін, ал қайсысын таңдау осы оператор орындалған кезде жүріс кезінде анықталады. Бұл бағдарламалаушыны қажетсіз шешімдер қабылдаудан босатады және бағдарламаларды формалды дамытуға көмектеседі. GCL бірнеше мәндерді тағайындау операторын қамтиды. Мысалы, оператордың орындалуы оң жақтағы мәндерді есептеу арқылы, содан кейін оларды сол жақтағы айнымалыларға сақтау арқылы жүзеге асырылады. Осылайша, бұл оператор мен айнымалыларының мәнін ауыстырады. GCL-ді қолдануды талқылайтын келесі кітаптар:
The Guarded Command Language (GCL) is a programming language defined by Edsger Dijkstra for predicate transformer semantics in EWD472. It combines programming concepts in a compact way. It makes it easier to develop a program and its proof hand in hand, with the proof ideas leading the way; moreover, parts of a program can actually be calculated. An important property of GCL is nondeterminism. For example, in the if statement, several alternatives may be true, and the choice of which to choose is done at runtime, when the if statement is executed. This frees the programmer from having to make unnecessary choices and is an aid in the formal development of programs. GCL includes the multiple assignment statement. For example, execution of the statement is done by first evaluating the righthand side values and then storing them in the lefthand variables. Thus, this statement swaps the values of and
The following books discuss the development of programs using GCL:
Қадағалаумен басқару
Күзетілетін команда – күзетілетін командалар тілінің ең маңызды элементе. Күзетілетін командада, атынан көрініп тұрғандай, команда "күзетпен" қамтамасыз етілген. Күзет – бұл тұжырым, ол осы оператор орындалуы алдында рас болуы тиіс. Оператордың орындалу басында, күзеттің рас екенін қарастыруға болады. Сондай-ақ, егер күзет жалған болса, оператор орындалмайды. Күзетілетін командаларды қолдану бағдарламаның талаптарға сәйкес келетінін дәлелдеуді жеңілдетеді. Оператор көбінесе тағы бір күзетілетін команда болып табылады.
The guarded command is the most important element of the guarded command language. In a guarded command, just as the name says, the command is "guarded". The guard is a proposition, which must be true before the statement is executed. At the start of that statement's execution, one may assume the guard to be true. Also, if the guard is false, the statement will not be executed. The use of guarded commands makes it easier to prove the program meets the specification. The statement is often another guarded command.
өткізіп тастау
skip және abort – күзетілген командалар тіліндегі маңызды операторлар. abort – бұл анықталмаған команда: ештеңе істемеуге болады. Оны тоқтатудың қажеті жоқ. Ол дәлелдеуді құрастыру кезінде бағдарламаны сипаттау үшін қолданылады, мұндай жағдайда дәлелдеу көбінесе сәтсіз аяқталады. skip – бұл бос команда: ештеңе істемеу. Ол бағдарламаның өзінде қолданылады, егер синтаксис оператор талап еткен кезде, бірақ күй өзгермеуі керек болса.
skip and abort are important statements in the guarded command language. abort is the undefined instruction: do anything. It does not even need to terminate. It is used to describe the program when formulating a proof, in which case the proof usually fails. skip is the empty instruction: do nothing. It is used in the program itself, when the syntax requires a statement but the state should not change.
Тапсырма
Айнымалыларға шамалар тағайындайды.
Assigns values to variables.
Таңдау: егер
Таңдау (көбінесе "шартты оператор" немесе "егер оператор" деп аталады) - сақшыланған командалардың тізімі, олардың бірі орындалуға таңдалады. Егер бірнеше сақшы дұрыс болса, сақшысы дұрыс болған бір оператор орындалу үшін кездейсоқ таңдалады. Егер ешбір сақшы дұрыс болмаса, нәтижесі белгісіз. Сақшылардың кем дегенде біреуі дұрыс болуы керек болғандықтан, бос оператор skip жиі қажет болады. if fi операторында сақшыланған командалар жоқ, сондықтан ешқандай дұрыс сақшы болмайды. Осылайша, if fi – тоқтату операторымен тең.
The selection (often called the "conditional statement" or "if statement") is a list of guarded commands, of which one is chosen to execute. If more than one guard is true, one statement whose guard is true is nondeterministically chosen to be executed. If no guard is true, the result is undefined. Because at least one of the guards must be true, the empty statement skip is often needed. The statement if fi has no guarded commands, so there is never a true guard. Hence, if fi is equivalent to abort.
Семантика
Таңдау орындалған кезде барлық күзетшілер тексеріледі. Егер күзетшілердің ешқайсысы да шын мәнді болмаса, таңдау орындалуы тоқтатылады, әйтпесе шын мәнді күзетшілердің бірі кездейсоқ таңдалып, сәйкес келетін оператор орындалады.
Upon execution of a selection all guards are evaluated. If none of the guards evaluates to true then execution of the selection aborts, otherwise one of the guards that has the value true is chosen non deterministically and the corresponding statement is executed.
Қайталау: орындаңыз
Бұл қайталаудың немесе циклдың орындалуы төменде көрсетілген.
Execution of this repetition, or loop, is shown below.
Семантика
Қайталауды орындау 0 немесе одан көп итерацияларды орындаудан тұрады, мұнда итерация (белгісіздікпен) Gi → Si түріндегі сақталған команданы таңдаудан тұрады, оның шартты өрнегі Gi шын мәнді береді және Si командасын орындаудан тұрады. Осылайша, егер барлық шартты өрнектер бастапқыда жалған болса, қайталау дереу аяқталады, ешқандай итерация орындалмайды. Сақталған командалары жоқ do od қайталауы 0 итерация орындайды, сондықтан do od командасы skip командасына тең.
Execution of the repetition consists of executing 0 or more iterations, where an iteration consists of (nondeterministically) choosing a guarded command Gi → Si whose guard Gi evaluates to true and executing the command Si. Thus, if all guards are initially false, the repetition terminates immediately, without executing an iteration. Execution of the repetition do od, which has no guarded commands, executes 0 iterations, so do od is equivalent to skip.
Құрылымы бойынша дұрыс бағдарламалар
Күзетілген командалардың бақылау сәйкестігін торға біріктіру Refinement Calculus-қа алып келді. Бұл B әдісі сияқты формалды әдістерде автоматтандырылған, бұл бағдарламаларды олардың сипаттамаларынан формалды түрде тудыруға мүмкіндік береді.
Generalizing the observational congruence of Guarded Commands into a lattice has led to Refinement Calculus. This has been mechanized in Formal Methods like B Method that allow one to formally derive programs from their specifications.
Үлгілерді тексеру
Сақталған командалар Promela бағдарламалау тілінде қолданылады, ол SPIN модельді тексерушісінде пайдаланылады. SPIN бір уақытта жұмыс істейтін бағдарламалық жасақтаманың дұрыс жұмыс істеуін растайды.
Guarded commands are used within the Promela programming language, which is used by the SPIN model checker. SPIN verifies correct operation of concurrent software applications.
Басқа
Perl модулі Commands::Guarded Дикстраның қорғалған командаларының детерминистік, түзетуге келтіретін түрін іске асырады.
The Perl module Commands::Guarded implements a deterministic, rectifying variant on Dijkstra's guarded commands.