<commit_before>% -*- root: ../main.tex -*-
\chapter{Introduction\label{chap:introduction}}

\paragraph{Abstract}

In this chapter we will introduce this \thisworkm. We will cover the motivation that lead me to develop this \thisworkm and which objectives does it have.

We will discuss its scope and some details of the linked list most general client and finally we will make a brief description of the whole document. 

\section{Motivation}

\label{Motivation}
On May $\text{2}^{\text{nd}}$ a Japanese satellite was lost. This satellite cost \$248 million.
%
Research shows it was a software error \cite{japaneseSatellite}. 
%
Last year, another software error was found in boeing-787.
%
Apparently, the plane’s electrical generators fall into a failsafe mode if kept continuously powered on for 248 days. \cite{boein787}
%
Fortunately this software error was discovered without relevant economic or human consequences.
%
Between 1985 and 1987 6 people died because of a software malfunction of a x-ray machine. \cite{xraykill}.
%
This are just a few example to show that Software verification is a very important problem.
%
One needs to be sure that the software being developed is correct, one would like it to work as expected with no bugs at all and every one would like its software to be perfect.
%
There are some critical software as the ones developed for aeroplanes, spaceships, nuclear reactors which can't have any errors while there are some other software which can afford some errors.


The usual approach its testing.
% 
The normal way to verify and validate a software is running test to find, whenever is possible, all the errors.
% 
When the software is finished (or even while it is being developed) one can test it to check it is correct.
%
How can one be sure that all functionalities have been proven? Maybe some test were missed and some bugs have not been found so the software is not correct.
%
As we said before, some systems can afford this issue but there are some others which can not.


In the other hand, as a mathematician, I am very used to mathematical proofs of theorems and I know logic is a very powerful tool.
%
We wonder if it were possible to verify and validate Software using those powerful tools.
%
And the answer is affirmative.
%
One can prove Software correctness in a formal way.
% 
Software correctness can be proven in the same way as the Gauss theorem can be proven.
%
One just need the appropriate framework, tools and of course, knowledge.


I have found this topic very useful and we wanted to explore a very formal verification of some theories.


\section{Objectives}

The goal is to prove the correctness of an implementation of linked list. \footnote{The specification of the implementation is on \ref{def:problem}}

We achieve to prove with mathematical certain the correctness of the program. We achieve to prove that a list is always a list and that it is always ordered, independently of the number of threads executing. Thus, there are 2 steps to prove. The first one is to prove that with just one process using the list, those properties are preserved always. The other one is with multiple processes using the same list (in a grain-lock implementation).

But to achieve any formal proof, we need some axioms to use.
We can't define absolute truth, we can just demonstrate that something is true, according to the truths we already know. 
We can prove some theorem, but we must use the axioms we consider true. 

So to achieve the verification, we need to obtain the axioms of the linked list theory.

\section{Scope}


\label{def:leap}

\section{Document Structure}

After this introduction, we will define some necessary concepts to understand deeply this \thisworkm. This preliminary includes the state of the art.


\section{Preliminaries}

\subsection{First order logic}

\paragraph{Notation}
\label{def:notation}
We assume the usual way of representing and working with \gls{FOL}, this is
\begin{itemize}
	\item \textbf{Symbols:} $\{),(, \implies, \dimplies, \orcond , \andcond \}$
	\item \textbf{Quantifiers:} $\{\forall, \exists\}$
	\item \textbf{Constants:} $\{\true,\false\}$
	where we define $\true$ as \textit{true} and $\false$ as \textit{false}.
\end{itemize}

One could consider $\exists x(P(x))$  as an abbreviation of $\neg (\forall x(\neg P(x)))$, but for better understanding we would use both quantifiers when needed.
We could also use $(a \orcond b)$ instead of $(\neg a \implies b)$ but, again, for the better understanding those abbreviations will be used.
The same happens with $\true \equiv \neg \false$, but it is clearer when we use both symbols and not just one of them.


\paragraph{Definitions}

We are going to define some very basic concepts, needed and used during the whole \thisworkmp.

We say a formula $F$ is \concept{satisfiable} \gls{iff} there exists an interpretation $I$ such that $I \vDash F$. 
%
We say a formula $F$ is \concept{valid} \gls{iff} for all interpretations $I$, $I\vDash F$.
\label{def:validity}
This 2 concepts are very important and they are very related. $F$ is valid \gls{iff} $\neg F$ is unsatisfiable. 


A first-order \concept{theory} is defined by the following components: 
\begin{itemize}
	\item Its \textbf{signature} $\Sigma$ is a set of constant, function and predicate symbols.
	\item Its set of \textbf{axioms} $\axioms$ is a set of \gls{FOL} closed formula in which only elements from $\Sigma$ appear.
\end{itemize}


There are some important properties than a theory may have. 

A theory $\Sigma$ is \concept[Completeness]{complete} \gls{iff} for every closed $\Sigma-$formula $\sigma$ we have $(\Sigma\vDash \sigma) \orcond (\Sigma\neg\vDash \sigma) $

A theory $\Sigma$ is \concept[Consistency]{consistent} if there is at least one $\Sigma-$interpretation.	Equivalently, a theory $\Sigma$ is consistent if $\Sigma \not\vDash \false$

If our theory is not consistent, we can have a formal proof of anything we want to prove. 
%
We can prove contradictions. 
%
We could prove that some program is both correct and incorrect, which gives us no information. 
%
Thus consistency is a fundamental property for this \thisworkm.

In the other hand, completeness is very desirable, but may not be possible to achieve because of the incompleteness theorem of Gödel.


It is not possible to have a complete and consistent theory while including basic arithmetical truths. 
%
One could expect that the theory needed to proof programs correctness wouldn't be complete. 
%
In that case, we will not be able to proof the incorrectness of a program.
%
Normally, consistency is basic while completeness is only desirable.

Another property of theories is the \textbf{decidability}. We say a theory $\Sigma$ is \concept{decidable} if $\Sigma \vDash F$ is decidable, for every $\Sigma-$formula 
and 
$F$ a $\Sigma-$formula is decidable if there is an \textbf{algorithm} that \textbf{always terminates} with ``yes'' if $F$ is valid in $\Sigma$ ($\Sigma$-valid) or ``no'' if $F$ is not $\Sigma-$valid.


Decidability is a stronger property of a theory than completeness. 
%
As completeness, decidability is a very desirable property but because \gls{FOL} (the theory with no axioms) is undecidable in general, we may not have decidability in the theory we are working on.



\begin{example}
\concept{Theory\IS of equality}

\label{theory:equality}

We are going to define the theory of equality, because it is the simplest first-order theory.

The signature of the theory is:

\[\Sigma_e:\{=,a,b,c,...\}\]

and it's axioms are:

\begin{description}
	\item[Reflexivity:	] $\forall x, x=X$
	\item[Symmetry:	] $\forall x,y x=y \implies y=x$
	\item[Transitivity:	] $\forall x,y,z x=y \andcond y=z \implies x=z$
	\item[Function congruence:] For each function $f$
	\[\forall \gor{x},\gor{y} \left( \bigwedge_{i=1}^n x_i = y_i \right) \implies f(\gor{x}) = f(\gor{y})\]
	\item[Predicate congruence:]  For each predicate $P$
	\[\forall \gor{x},\gor{y} \left( \bigwedge_{i=1}^n x_i = y_i \right) \implies f(\gor{x}) \dimplies f(\gor{y})\]

	This 2 ``axioms'' are not axioms but an \concept[Axioms schema]{axiom schema}, because there is one axiom for each function $f$ or predicate $p$.
\end{description}

\gls{FOL} with equality is a decidable theory as <NAME> proved in 1915 \cite{EqualityIsDecidable}. It is consistent and complete.<commit_msg>Introduction finished. Wondering if program correctness should be in the introduction too or it is design<commit_after>% -*- root: ../main.tex -*-
\chapter{Introduction\label{chap:introduction}}

\paragraph{Abstract}

In this chapter we will introduce this \thisworkm. We will cover the motivation that lead me to develop this \thisworkm and which objectives does it have.

We will discuss its scope and some details of the linked list most general client and finally we will make a brief description of the whole document. 

\section{Motivation}

\label{Motivation}
On last May $\text{2}^{\text{nd}}$ a Japanese satellite was lost. This satellite cost \$248 million.
%
Research shows it was a software error \cite{japaneseSatellite}. 
%
Last year, another software error was found in boeing-787.
%
Apparently, the plane’s electrical generators fall into a failsafe mode if kept continuously powered on for 248 days. \cite{boein787}
%
Fortunately this software error was discovered without relevant economic or human consequences.
%
Between 1985 and 1987 6 people died because of a software malfunction of a x-ray machine. \cite{xraykill}.
%
This are just a few example to show that Software verification is a very important problem.
%
One needs to be sure that the software being developed is correct, one would like it to work as expected with no bugs at all and every one would like its software to be perfect.
%
There are some critical software as the ones developed for aeroplanes, spaceships, nuclear reactors which can't have any errors while there are some other software which can afford some errors.


The usual approach its testing.
% 
The normal way to verify and validate a software is running test to find, whenever is possible, all the errors.
% 
When the software is finished (or even while it is being developed) one can test it to check it is correct.
%
How can one be sure that all functionalities have been proven? Maybe some test were missed and some bugs have not been found so the software is not correct.
%
As we said before, some systems can afford this issue but there are some others which can not.


In the other hand, as a mathematician, I am very used to mathematical proofs of theorems and I know logic is a very powerful tool.
%
We wonder if it were possible to verify and validate Software using those powerful tools.
%
And the answer is affirmative.
%
One can prove Software correctness in a formal way.
% 
Software correctness can be proven in the same way as the Gauss theorem can be proven.
%
One just need the appropriate framework, tools and of course, knowledge.


I have found this topic very useful and we wanted to explore a very formal verification of some theories.


\section{Objectives}

The goal is to prove the correctness of an implementation of a concurrent linked list. \footnote{The specification of the implementation is on \ref{def:problem}}

We achieve to prove with mathematical certain the correctness of the program. 
%
We achieve to prove that a list is always a list and that it is always ordered, regardless the number of threads executing.
%
Thus, there are 2 steps to prove. 
%
The first one is to prove that with just one process using the list, those properties are preserved always. 
%
The other one is with multiple processes using the same list. 
%
In particular, in a grain-lock implementation.

But to achieve any formal proof, we need some axioms as a basis.
%
We can't define absolute truth, we can just demonstrate that something is true, according to the truths we already know. 
%
We can prove some theorem, but we must use the axioms we consider true. 
%
So to achieve the verification, we need to obtain the axioms of the linked list theory.

It is essential to build a framework in which this verification can be automatized, so first order logic will be used. 
%
Additionally, it is to be hoped that this \gls{FOL} proofs can be generated, stored and checked by third-parties.


\section{Scope}

\label{def:leap}



\section{Document Structure}

After this introduction, we will define some necessary concepts to understand deeply this \thisworkm. 

Once the reader is familiarized with some basic concepts, the state of the art is covered. 
%
We show some of the actual technologies even commercial products used nowadays.
%
This projects state that it is a not main-frame but not new scope of research.

Chapter three has a preliminary section of what formal verification is and when and why a program can be formally verified and validated as correct. 
% 
After that general preliminaries, the \gls{FOL} theories used and the formalism necessary to do formal verification is explained.
%
The implementation of the structure is defined in this chapter.

Once the goal and the formalism is defined, the development can be fully understand. 
%
In chapter four, the methodology used the tools developed or used are described.

Next, the results of the work can be shown. 
%
This chapter gadders the list of axiom needed, an analysis of the \gls{FOL} proofs generated and finally a time analysis.

At last, the work is summarized in its conclusions. 
%
Does formal verification worth the try? 


\section{Preliminaries}

\subsection{First order logic}

\paragraph{Notation}
\label{def:notation}
We assume the usual way of representing and working with \gls{FOL}, this is
\begin{itemize}
	\item \textbf{Symbols:} $\{),(, \implies, \dimplies, \orcond , \andcond \}$
	\item \textbf{Quantifiers:} $\{\forall, \exists\}$
	\item \textbf{Constants:} $\{\true,\false\}$
	where we define $\true$ as \textit{true} and $\false$ as \textit{false}.
\end{itemize}

One could consider $\exists x(P(x))$  as an abbreviation of $\neg (\forall x(\neg P(x)))$, but for better understanding we would use both quantifiers when needed.
We could also use $(a \orcond b)$ instead of $(\neg a \implies b)$ but, again, for the better understanding those abbreviations will be used.
The same happens with $\true \equiv \neg \false$, but it is clearer when we use both symbols and not just one of them.


\paragraph{Definitions}

We are going to define some very basic concepts, needed and used during the whole \thisworkmp.

We say a formula $F$ is \concept{satisfiable} \gls{iff} there exists an interpretation $I$ such that $I \vDash F$. 
%
We say a formula $F$ is \concept{valid} \gls{iff} for all interpretations $I$, $I\vDash F$.
\label{def:validity}
This 2 concepts are very important and they are very related. $F$ is valid \gls{iff} $\neg F$ is unsatisfiable. 


A first-order \concept{theory} is defined by the following components: 
\begin{itemize}
	\item Its \textbf{signature} $\Sigma$ is a set of constant, function and predicate symbols.
	\item Its set of \textbf{axioms} $\axioms$ is a set of \gls{FOL} closed formula in which only elements from $\Sigma$ appear.
\end{itemize}


There are some important properties than a theory may have. 

A theory $\Sigma$ is \concept[Completeness]{complete} \gls{iff} for every closed $\Sigma-$formula $\sigma$ we have $(\Sigma\vDash \sigma) \orcond (\Sigma\neg\vDash \sigma) $

A theory $\Sigma$ is \concept[Consistency]{consistent} if there is at least one $\Sigma-$interpretation.	Equivalently, a theory $\Sigma$ is consistent if $\Sigma \not\vDash \false$

If our theory is not consistent, we can have a formal proof of anything we want to prove. 
%
We can prove any contradiction. 
%
We could prove that some program is both correct and incorrect at the same time, which gives no information. 
%
Thus \textbf{consistency is a fundamental property} for this \thisworkm.

In the other hand, completeness is very desirable, but may not be possible to achieve because of the incompleteness theorem of Gödel.
%
It is not possible to have a complete and consistent theory while including basic arithmetical truths. 
%
One could expect that the theory needed to prove programs correctness would not be complete, because of the inclusion of basic arithmetical truths. 
%
Normally, consistency is basic while completeness is only desirable.

Another property of theories is the \textbf{decidability}. 
%
We say a theory $\Sigma$ is \concept{decidable} if $\Sigma \vDash F$ is decidable, for every $\Sigma-$formula 
where 
$F$ a $\Sigma-$formula is decidable if there is an \textbf{algorithm} that \textbf{always terminates} with ``yes'' if $F$ is valid in $\Sigma$ ($\Sigma$-valid) or ``no'' if $F$ is not $\Sigma-$valid.


Decidability is a stronger property than completeness. 
%
As completeness, decidability is a very desirable property but because \gls{FOL} (the theory with no axioms) is undecidable in general, we may not have decidability in the theory we are working on.



\begin{example}
\concept{Theory\IS of equality}

\label{theory:equality}

We are going to define the theory of equality, because it is the simplest first-order theory.

The signature of the theory is:

\[\Sigma_e:\{=,a,b,c,...\}\]

and it's axioms are:

\begin{description}
	\item[Reflexivity:	] $\forall x, x=X$
	\item[Symmetry:	] $\forall x,y x=y \implies y=x$
	\item[Transitivity:	] $\forall x,y,z x=y \andcond y=z \implies x=z$
	\item[Function congruence:] For each function $f$
	\[\forall \gor{x},\gor{y} \left( \bigwedge_{i=1}^n x_i = y_i \right) \implies f(\gor{x}) = f(\gor{y})\]
	\item[Predicate congruence:]  For each predicate $P$
	\[\forall \gor{x},\gor{y} \left( \bigwedge_{i=1}^n x_i = y_i \right) \implies f(\gor{x}) \dimplies f(\gor{y})\]

	This 2 ``axioms'' are not axioms but \concept[Axiom schema]{axiom schemas}, because there is one axiom for each function $f$ or predicate $p$.
\end{description}

\gls{FOL} with equality is a decidable theory as <NAME> proved in 1915 \cite{EqualityIsDecidable}. 
%
It is both consistent and complete.
{'fraction_non_alphanumeric': 0.08045532408686523, 'fraction_numerical': 0.0034259822069956348, 'mean_word_length': 4.202069560218454, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 5, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '6774379', 'n_tokens_mistral': 5206, 'n_tokens_neox': 4922, 'n_words': 2654}