SpecVer in english - Historia wersji

AndrzejSalwicki o 09:53, 12 lip 2025

2025-07-12T09:53:14Z

AndrzejSalwicki o 09:46, 12 lip 2025

2025-07-12T09:46:20Z

AndrzejSalwicki o 06:59, 12 lip 2025

2025-07-12T06:59:44Z

AndrzejSalwicki o 06:58, 12 lip 2025

2025-07-12T06:58:44Z

AndrzejSalwicki o 06:56, 12 lip 2025

2025-07-12T06:56:15Z

AndrzejSalwicki o 06:55, 12 lip 2025

2025-07-12T06:55:08Z

AndrzejSalwicki o 06:49, 12 lip 2025

2025-07-12T06:49:02Z

AndrzejSalwicki: tłimaczenie

2025-07-11T17:44:53Z

tłimaczenie

Nowa strona

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 algorithmic 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

( MSS 2007 ↓ ) Grażyna Mirkowska, Andrzej Salwicki, Oskar Świda. Algorithmic Logic + SpecVer = the methodology for high integrity programming . "Fundamenta Informaticae", pp. 1-17, 2008.
( MSS 2008 ↓ ) Grażyna Mirkowska, Andrzej Salwicki, Oskar Świda. Verifying a Class: Combining Testing and Proving . "Fundamenta Informaticae", 2009.
( MS 2015 ↓ ) Grażyna Mirkowska, Andrzej Salwicki. Proving simulation class . , 2015.
( MS 2018 ↓ ) Grażyna Mirkowska, Andrzej Salwicki: Enlightened programmer . 2018.

Category :

SpecVer

Navigation menu

Login and registration

Side
Discussion

Read
Source text
View history

Home page
Recent changes
Random page
Help

Tools

Linking
Changes in linked
Special pages
Printable version
Link to this version
Information about this site

This page was last modified at 11:16, 16 Mar 2020.
This page has been viewed 180,413 times.

Confidentiality Policy
About Lem
Legal information

Powered by MediaWiki

@@ Linia 18: / Linia 18: @@
 ''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:
+SpecVer is  a project in which documents of at least three types will coexist:
      * specifications,

← poprzednia wersja		Wersja z 09:46, 12 lip 2025
Linia 1:		Linia 1:
−	~~=== Tekst nagłówka ===~~
−	~~SpecVer~~
	Contents		Contents

@@ Linia 15: / Linia 15: @@
 Bibliography
-== Constructing and analyzing software using calculus of programs <math>AL</math> (''aka'' Algoritmic logic). ==
+== Constructing and analyzing software using calculus of programs <math>\mathcal
 ''A riddle'' . Try it out - can you formulate a thesis about PawelG's program and provide proof?

@@ Linia 15: / Linia 15: @@
 Bibliography
-== Constructing and analyzing software using calculus of programs AL (''aka'' Algoritmic logic). ==
+== Constructing and analyzing software using calculus of programs <math>AL</math> (''aka'' Algoritmic logic). ==
 ''A riddle'' . Try it out - can you formulate a thesis about PawelG's program and provide proof?
@@ Linia 141: / Linia 141: @@
      oral statement, ca. 1976
 == Bibliography ==

@@ Linia 143: / Linia 143: @@
-== Bibliografia ==
+== 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 }}

@@ Linia 143: / Linia 143: @@
-Bibliography
+== Bibliografia ==
+# ({{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 }}
-    ( MSS 2007 ↓ ) Grażyna Mirkowska, Andrzej Salwicki, Oskar Świda. Algorithmic Logic + SpecVer = the methodology for high integrity programming . "Fundamenta Informaticae", pp. 1-17, 2008.
+# ({{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 }}
-    ( MSS 2008 ↓ ) Grażyna Mirkowska, Andrzej Salwicki, Oskar Świda. Verifying a Class: Combining Testing and Proving . "Fundamenta Informaticae", 2009.
+# ({{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  }}
-    ( MS 2015 ↓ ) Grażyna Mirkowska, Andrzej Salwicki. Proving simulation class . , 2015.
+# ({{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=  }}
-    ( MS 2018 ↓ ) Grażyna Mirkowska, Andrzej Salwicki: Enlightened programmer . 2018.
+[[Category:SpecVer]]
-−
 Category :
-−
-    SpecVer

@@ Linia 1: / Linia 1: @@
+=== Tekst nagłówka ===
 SpecVer
 Contents
@@ Linia 15: / Linia 15: @@
 Bibliography
-Constructing and analyzing software using algorithmic logic.
+== Constructing and analyzing software using calculus of programs AL (''aka'' Algoritmic logic). ==
-A riddle . Try it out - can you formulate a thesis about PawelG's program and provide proof?
+''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,
+     * specifications,
-     modules of classes, procedures, functions, etc.,
+    *     modules of classes, procedures, functions, etc.,
-     documents containing arguments that determine the correctness of the module with respect to the specification.
+    *     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
@@ Linia 52: / Linia 52: @@
      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 graphs,
-             Algorithmic theory of numbers
+            *             Algorithmic theory of numbers
-             Algorithmic theory of ...
+            *             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.
@@ Linia 73: / Linia 73: @@
      Algorithmic stack theory enjoys the following property, which is close to categorical.
-Representation theorem
+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
@@ Linia 84: / Linia 85: @@
 see Proof of the above property
-Algorithmic theory of natural numbers
+=== 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.
@@ Linia 151: / Linia 152: @@
 Category :
      SpecVer
-−
-Navigation menu
-−
-    Login and registration
-−
-    Side
-    Discussion
-−
-    Read
-    Source text
-    View history
-−
-    Home page
-    Recent changes
-    Random page
-    Help
-−
-Tools
-−
-    Linking
-    Changes in linked
-    Special pages
-    Printable version
-    Link to this version
-    Information about this site
-−
-    This page was last modified at 11:16, 16 Mar 2020.
-    This page has been viewed 180,413 times.
-−
-    Confidentiality Policy
-    About Lem
-    Legal information
-−
-    Powered by MediaWiki