Tekst źródłowy strony SpecVer in english

=== Tekst nagłówka ===
SpecVer
Contents

    1 Constructing and analyzing software using algorithmic logic.
    2. Example of analysis performed using program calculus
    3 Algorithmic Stack Theory
    4. Algorithmic FIFO Queuing Theory
    5 Algorithmic Theory of Binary Search Trees
    6 Algorithmic theory of natural numbers
    7 Tools
    8 See also
    9 Notes
    10 Footnotes
    11 Bibliography

== Constructing and analyzing software using calculus of programs <math>\mathcal
{AL}</math> (''aka'' Algoritmic logic). ==

''A riddle'' . Try it out - can you formulate a thesis about PawelG's program and provide proof?

We propose a project in which documents of at least three types will coexist:

    * specifications,
    *     modules of classes, procedures, functions, etc.,
    *     documents containing arguments that determine the correctness of the module with respect to the specification.

The SpecVer project is undoubtedly challenging. But I think we have an original idea. See the Case Study
before we go into further detail:

    we will develop algorithmic theories of various structures and investigate their connections with the relevant classes,
    As a test of our approach, we propose building a class library similar to the well-known STL library. The difference is that the final product should include for each class:

        specification of the class - or in other words the signature and axioms of the algorithmic theory describing not only the operation interface, but also the properties of operations on objects described by the class,K

TK
implementation , i.e. class ,K
verification , i.e. proof that the class ensures the truth of all properties listed in the axioms of the theoryK
TK


Today it is certainly too early to think about a complete description of this project.

The materials we post here are intended to show our way of thinking and directions of research.

Professor Józef Winkowski [1] once casually said that "creating a larger programming system is a work similar to building many mathematical theories" . Today we can precisely justify this idea. More precisely, we mean that it is not enough to create software modules or interfaces. We need specifications. We have to think about specifications in the same way as about axiomatizations of formalized theories and therefore we have to investigate the problems of consistency, completeness, and categoricality. Moreover, when creating verdicts verifying correctness, we create algorithmic theories and we use the theorems of these theories in further work on subsequent programs.

We will try to illustrate this idea with a few examples...

Proposal:

    For years, we have been postulating the creation and development of algorithmic theories (formalized or not) see the work Algorithmic theory of stacks, chapter IV of the book Algorithmic Logic, ...
    it may seem that our suggestions have met with a positive response when you notice that monographs are being written:

            * Algorithmic theory of graphs,
            *             Algorithmic theory of numbers
            *             Algorithmic theory of ...

        But that's not exactly what we're proposing. These books cover algorithms and their analysis, and theorems about algorithms. However, all of this is formulated in a traditional way, in first-order language. 

    We believe that algorithmic theories should use a language in which, in addition to first-order formulas, there are programs (algorithms) and algorithmic formulas. It's not a bad thing if the axiom set of an algorithmic theory includes algorithmic formulas. The theorems of an algorithmic theory are algorithmic formulas that can be proven in algorithmic logic. Axiomatizations of algorithmic theories can greatly benefit from including one or more algorithmic formulas among the axioms. See the books Algorithmic Logic, p. ..., and Algorithmic Logic for Programmers, p.

Example of analysis performed using program calculus

One of our best-documented programs is a bank simulation program. A presentation discussing the principle of factoring a programming task into subtasks involving class specification, their implementation, and subsequent verification (i.e., proving the correctness of the constructed class with its specification) can be found here . If you'd like, view the full text of the bank branch simulation program . A significant part of this program is the Simulation class and two auxiliary classes for Simulation. The Simulation class implements a language supporting the simulation task and is reused many times. Therefore, we took the trouble to provide the specification of this class. This means that programmers using the Simulation class don't need to read it or learn the implementation details. In the paper "Proving Simulation Class," we proved that this class correctly implements the specification. It's worth noting that the Simulation class and the two auxiliary classes together comprise over 250 lines of Loglan program. We also recommend reading two papers on SpecVer technology and on proving the correctness of the PriorityQueues auxiliary class implementation.
Algorithmic stack theory

Algebraic or algorithmic specification of stacks? Recall that the inspiration for creating algebraic specifications of data structures stemmed from the need to simplify the transformation of Boolean expressions appearing in conditional if statements and iterative while statements . It's a pity that researchers didn't ask themselves basic questions: is the specification complete? Does it create a decidable theory? Instead, the concept of a sufficiently complete specification was formulated. See Barbara Liskov and John Guttag's book Abstraction and Specification in Program Development , MIT Press, 1986.

Meanwhile, it turned out that, for example:

    First-order stack theory is decidable, see
    This theory has non-standard programmable models! That is, you can write a program in which the stack class is written in such a way that certain objects of this class, i.e., certain stacks, will behave like infinite stacks.
    Algorithmic stack theory enjoys the following property, which is close to categorical.

Representation '''theorem'''

Any two models of algorithmic stack theory that contain the same set of elements are isomorphic.
Algorithmic FIFO Queuing Theory

=== Algorithmic Binary Search Tree Theory ===

We wrote about this theory in "Algorithmic Logic for Programmers." It turned out that another axiomatization can be given. We proved the property

B ST⊢( ∀ n ∈ NFrome ) ( ∀ e ∈ El e m ) [ c a l l i n s e r t ( e , n ) ] m e m b e r ( e , n )  

see Proof of the above property
=== Algorithmic theory of natural numbers ===

I believe that it is necessary to develop a theory that will combine several different theories into one whole: the theory of natural numbers, the theory of recursive functions, the analysis of algorithms performing computations in the domain of natural numbers (the so-called algorithmic theory of natural numbers. theoretical arithmetic.
Axioms of the algorithmic theory of natural numbers
A1) A2) A3) From these three axioms we can derive all the axioms of Peano theory, including the induction scheme.∀ x{ y: = 0 ;while  ¬x=y to  y: = y+ 1  from } ( x = y)

∀ x¬ x + 1 = 0

∀ x ∀ y( x + 1 = y+ 1 ) → x = y



Let's consider some examples:

    Euclidean algorithm - how to prove the correctness of this algorithm? It does not follow from the Peano axioms. However, from the algorithmic axiom that a natural number is a natural number, the algorithmic formula follows. From this algorithmic formula, an algorithmic formula expressing the halting property of the Euclidean algorithm follows.∀ x { while  ¬ x = 0  to  y: = y− 1  from } ( x = 0 )

    Collatz problem - this simple algorithm can have infinite computations in a non-standard model of natural numbers with addition,
    Fermat's Last (Great) Theorem states, among other things, that a certain fairly simple program has an infinite computation. Andrew Wiles's proof is over 200 pages long.
    Many hypotheses remain unanswered. However, it is known that if they are true, their proofs can be based on three axioms and the deductive system of algorithmic logic.


Language = <Alphabet, Well-Constructed Expressions>

Correctly Constructed Expressions are

    - thermal baths, 
    - first-order formulas, contain a subset of open formulas, i.e. formulas without quantifiers, 
    - programs, 
    - algorithmic formulas. 

Specific axioms of this theory

Axioms of Algorithmic Logic

Inference rules of algorithmic logic

go to the Algorithmic Arithmetic page
Tools

The work of a person verifying a given software P against a given specification S should be supported by many tools. One of many (not existing yet) is

evidence editor

Another tool that should be developed is a proof-checker . However, the Mizar system I'm familiar with isn't suitable for our purposes. Mizar uses a first-order language, i.e., a predicate language. In our work, we use the <<EXAMPLE>> algorithmic formula language.

What features should the new proof-checker have? First of all, it should be constructed over a language of algorithmic formulas. (Perhaps over a class of algorithmic languages.) Secondly, in the proofs, we will use the inference rules of algorithmic logic. The specific axioms of the theories in which we will perform proofs can be formulas containing <<EXAMPLE>> programs.

Apparently, many software verification tasks are easy enough to attempt automatic proof (or counterexample construction). For such purposes, we should have a prover or systems with similar capabilities.
See also

    Memory garbage collection

Comments
Footnotes

    oral statement, ca. 1976

== Bibliography ==
# ({{odn|ref=nie|MSS|2007}}){{cytuj pismo|odn=tak|nazwisko=Mirkowska|imię=Grażyna|nazwisko2=Salwicki|imię2=Andrzej|nazwisko3=Świda|imię3=Oskar| tytuł=Algorithmic Logic + SpecVer = the methodology for high integrity programming|czasopismo=Fundamenta Informaticae|rok=2008|strony=1-17 |url=http://lem12.uksw.edu.pl/images/1/10/AL%2BSpecVer.pdf }}
# ({{odn|ref=nie|MSS|2008}}){{cytuj pismo|odn=tak|nazwisko=Mirkowska|imię=Grażyna|nazwisko2=Salwicki|imię2=Andrzej|nazwisko3=Świda|imię3=Oskar| tytuł=Verifying a Class: combining Testing and Proving|czasopismo=Fundamenta Informaticae|rok=2009|strony= |url=http://lem12.uksw.edu.pl/images/e/ef/Experimenting_Proving.pdf }}
# ({{odn|ref=nie|MS|2015}}){{cytuj pismo|odn=tak|nazwisko=Mirkowska|imię=Grażyna|nazwisko2=Salwicki|imię2=Andrzej|  tytuł=Proving simulation class|czasopismo= |rok=2015 |strony= |url=http://lem12.uksw.edu.pl/images/4/41/ProvingSimulation.pdf  }} 
# ({{odn|ref=nie|MS|2018}}){{cytuj książkę|odn=tak|nazwisko=Mirkowska|imię=Grażyna|nazwisko2=Salwicki|imię2=Andrzej|  tytuł=Światły programista|czasopismo= |rok=2018 |strony= |url=  }} 
[[Category:SpecVer]]