Commit 8a62aa10 authored by Dennis Müller's avatar Dennis Müller
Browse files

merge

parent f7a206d0
...@@ -69,7 +69,7 @@ In practice, theory parameters are often used in PVS for the signature of an abs ...@@ -69,7 +69,7 @@ In practice, theory parameters are often used in PVS for the signature of an abs
Given that the same practice is used in few other systems (if any), finding views without treating theory parameters in some way will not give us any useful results on these theories. We offer three approaches to handling these situations: Given that the same practice is used in few other systems (if any), finding views without treating theory parameters in some way will not give us any useful results on these theories. We offer three approaches to handling these situations:
\begin{enumerate} \begin{enumerate}
\item We can simply treat references to theory parameters as free variables and turn them into holes. Includes of parametric theories with arguments are turned into simple includes. \item \emph{Simple treatment:} We can interpret references to theory parameters as free variables and turn them into holes. Includes of parametric theories with arguments are turned into simple includes.
\item \emph{Covariant treatment:} We introduce new constants for the theory parameters and replace occurences of the parameters by constant references. Includes with parameters are again replaced by normal includes. \item \emph{Covariant treatment:} We introduce new constants for the theory parameters and replace occurences of the parameters by constant references. Includes with parameters are again replaced by normal includes.
...@@ -83,11 +83,11 @@ Given that the same practice is used in few other systems (if any), finding view ...@@ -83,11 +83,11 @@ Given that the same practice is used in few other systems (if any), finding view
\end{enumerate} \end{enumerate}
The first approach is the most straight-forward, but will lead to many false positives and negatives. The first approach is the most straight-forward, but will lead to many false positives and negatives.
We conjecture that the second approach is most useful for inter-library search, since it most closely corresponds to formalizations of abstract theories in other systems. A problem here is that the newly introduced constants are not pass on to includes without additional tranformations. We conjecture that the second approach is most useful for inter-library search, since it most closely corresponds to formalizations of abstract theories in other systems. A problem here is that the newly introduced constants are not passed on to includes with the same arguments without additional tranformations.
The third approach would turn every occurence of e.g. group-related symbols into function applications, which is a rather rare practice in most other systems. However, since this treatment of theory parameters comes closest to the semantics of the parameters, we conjecture that it is the most useful approach for intra-library viewfinding between PVS theories. The third approach would turn every occurence of e.g. group-related symbols into function applications, which is a rather rare practice in most other systems. However, since this treatment of theory parameters comes closest to the semantics of the parameters, we conjecture that it is the most useful approach for intra-library viewfinding between PVS theories.
\paragraph{} Additionally to the theory parameter related normlalization, we use the following techniques: \paragraph{} Additionally to the theory parameter related normalization, we use the following techniques:
\begin{itemize} \begin{itemize}
\item We curry function types $(A_1 \times\ldots A_n)\to B$ to $A_1 \to \ldots \to A_n\to B$. We treat lambda-expressions and applications accordingly. \item We curry function types $(A_1 \times\ldots A_n)\to B$ to $A_1 \to \ldots \to A_n\to B$. We treat lambda-expressions and applications accordingly.
...@@ -104,12 +104,23 @@ Given that the same practice is used in few other systems (if any), finding view ...@@ -104,12 +104,23 @@ Given that the same practice is used in few other systems (if any), finding view
\end{newpart} \end{newpart}
\subsection{Implementation}\label{sec:pvs} \subsection{Implementation}\label{sec:pvs}
\paragraph{} Using the above normalization methods, we can examplary write down a theory for a commutative binary operator using the Math-in-the-Middle foundation, while targeting e.g. the PVS Prelude library -- allowing us to find all commutative operators, as in Figure \ref{fig:use:pvs}.
We have tried the first two approaches regarding theory parameters -- i.e. the simple and covariant treatments -- to both inter- and intra-library viewfinding problems. Concretely, we have used a simple theory of Monoids in the Math-in-the-Middle foundation and the theory of Monoids in the NASA library as domains with the whole NASA library as target. The results are summarized in Figure \ref{fig:pvsresults}.
\begin{figure}[ht]\centering
\begin{tabular}{l | l || c | c}
\textbf{Domain} & \textbf{Normalization} & \textbf{Simple Morphisms} & \textbf{Aggregated} \\\hline
bla & bla & bla & bla
\end{tabular}
\caption{Results of Inter- and Intra-Library Viewfinding in the PVS NASA Library}\label{fig:pvsresults}
\end{figure}
\paragraph{} As an additional use case, we can examplary write down a theory for a commutative binary operator using the MitM foundation, while targeting the PVS Prelude library -- allowing us to find all commutative operators, as in Figure \ref{fig:use:pvs} (using the simple approach to theory parmeters).
\begin{figure}[ht]\centering \begin{figure}[ht]\centering
\fbox{\includegraphics[width=\textwidth]{pvs}} \fbox{\includegraphics[width=\textwidth]{pvs}}
\caption{Searching for Commutative Operators in PVS}\label{fig:use:pvs} \caption{Searching for Commutative Operators in PVS}\label{fig:use:pvs}
\end{figure} \end{figure}
\ednote{8 results for NASA, but NASA doesn't work in jEdit because of limited memory}
This example also hints at a way to iteratively improve the results of the viewfinder: since we can find properties like commutativity and associativity, we can use the results to in turn inform a better normalization of the theory by exploiting these properties. This in turn would potentially allow for finding more views. This example also hints at a way to iteratively improve the results of the viewfinder: since we can find properties like commutativity and associativity, we can use the results to in turn inform a better normalization of the theory by exploiting these properties. This in turn would potentially allow for finding more views.
\ No newline at end of file
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment