Izbrane teme sodobne fizike in matematike

Diagrami invariant za Turingove stroje

Diagrami invariant so bili uvedeni z namenom lažje zasnove dokazljivo pravilnih programov. V tem članku bodo uporabljeni za zasnovo in dokazovanje pravilnosti Turingovih strojev. Najprej bodo definirani splošni diagrami invariant ter njihova semantika in programska logika. Ti bodo uporabljeni za sestavo diagramov invariant za Turingove stroje. Za lažje dokazovanje bo uvedeno še nekaj notacije in pravil za sklepanje z njimi. Na koncu bodo uporabljeni na primeru.

Invariant diagrams for Turing machines

Invariant diagrams were created to facilitate the design of provably correct programs. In this paper, they will be used to design and prove the correctness of Turing machines. Firstly, general invariant diagrams, their semantics, and their program logic will be defined. They will be used to construct invariant diagrams for Turing machines. To facilitate the proofs, some notation and rules will be introduced for reasoning with them. Finally, their application will be demonstrated on an example.

avtor: Janez Ignacij Jereb
številka: 2
letnik: 13

PDF (0.3 Mb)

Vsi članki iz te številke

© 2025 Fakulteta za matematiko in fiziko Univerze v Ljubljani

Članke, objavljene pred septembrom 2025, lahko obiskovalci berejo, brskajo in/ali prenesejo za osebno in nekomercialno uporabo. Te vsebine je prepovedano reproducirati, spreminjati, prilagajati, objavljati ali prodajati brez pisnega soglasja avtorja članka in nosilca avtorskih pravic v citatu. Članki, objavljeni septembra 2025 in kasneje, so objavljeni pod licenco CC BY 4.0 oziroma izjemoma CC BY SA 4.0. Informacije o licenci so navedene v člankih.

For articles published before September 2025, readers may view, browse, and/or download material for temporary copying purposes only, provided these uses are for noncommercial personal purposes. That material may not be further reproduced, distributed, modified, adapted, published, or sold in whole or part, without prior written permission frm the author and copyright owner as cited. Articles published in September 2025 and later are instead provided under the terms of the CC BY 4.0 or CC BY SA 4.0 licenses. License information is available in each article.