useConceptionsGuidePrep.tex

\documentclass[]{article}

%opening
\title{}
\author{}

\begin{document}

\maketitle

\begin{abstract}

\end{abstract}

\section{Use of Conceptualizations}
Suppose we wish to incorporate into our curriculum on software engineering, material on both verification by formal methods, and also code derivation from specifications.
We might wish to have our students able to recognize a specification that can be satisfied by a transition system, so that they can ascertain that a representation of that transition system that can be converted automatically into a code implementation is an available approach.
We would need it to be, that the mathematical arguments for the transformations of requirements to Floyd-Hoare triples, for example,  convince the students.
Knowing the range of the state of preparedness of the incoming students allows us to plan the amount of time to devote to background material, and which background material should be provided.

Suppose we wished to make use of higher order logic, so that we could employ relations as arguments to functions.
We might, for example, wish to pass a graph constraining how a computation should be carried out.

We would like the students to appreciate the mapping between a recursive implementation and proof by mathematical induction.
We would like the students to discern when a recursion is a tail recursion.
We would like the students to appreciate the mapping between a tail recursion and iteration.

On the one hand we know which mathematical tools we wish to use, and on the other hand we have an idea of the extent of the students' conceptualizatons. With these we can begin to design an instructional approach.

\subsection{Recognize a specification that can be satisfied by a transition system}
For this, they should know what a transition system is:
There is a state, so we wish to represent a store, and the states it may take on.
There is a way to change the state, so we wish to represent transitions, and the idea of a path from state to state.
They should understand how a transition system can be represented in code, and that this can be carried out automatically.
Path algebra furnishes a rigourous description of these processes.
Path algebra ought to be accessible. to the students.
We could introduce (typed) lanbda calculus to the students with path algebra as its first use.
Now that we have Java 8 which provides anonymous functions, we can also offer a coded version for exploration.

\subsubsection{Instructions}
Having the use of typed lanbda calculus for path algebra, we can then use it to describe the effect of instructions in the context of Floyd-Hoare triples.

\subsubsection{Derivation}
Program derivation can be illustrated. Because we always prefer the students to apply what they comprehend, it is important to have exercises. Students should perform derivation, so that they come to appreciate that it can be automated.

\subsection{Composition}
Because derived components can be expected to be composed, either in sequence or in parallel, it is important that the students understand this at a rigorous level. As we can expect to be passing as arguments, procedures to be composed, the need for higher order logic is evident.

\subsection{Invariants}
The role of invariants in assuring the correctness of composition provides motivation for consideration of invariants.

\subsection{Provability}
With transition systems as a first example of what can be correct by construction, and invariant as a tool for provability, students can see that a way to design code with the prospect of fewer bugs is possible, at least in some circumstances.

\subsection{Use of Bridging Material}
The material on mathemtatical tools we wish to use should be introduced at a level that addresses the conceptualizataions the students bring to the course. 
Because the students bring different levels of preparedness to the class, some self-assessment might be included, to guide the student to the starting point corresponding to his or her current ideas.
The self-assessment can make use of the concepts used in the course. 
For example, during the course, the idea of invariants is used. 
Self-assessment can include questions posed to determine a student's understanding of the nature and role of an invariant, and direct the student to explanations that may be helpful, according to the results of the self-assessment. 

From this vantage point, other techniques of proving, including contradiction and contrapositive, are motivated.



\subsection{Summary}
The less-developed end of the range in the students' conceptualizations identifies the starting point  of explanatory background  material that should be provided.
The needs of the course determine the ending point of the explanatory background material.

The major themes in the students' conceptualizations highlight the critical aspects that distinguish one conceptualization from another, and therefore suggest the self-assessment questions that should be furnished, to help students know where to begin improving. 
An alternative to having analyzed the conceptualizations among the students is to use on a student case-by-case basis, a sort of failure modes and effects analysis, whereby the effect of lacking a certain understanding can be predicted to cause a certain pattern of confusion on the part of the student, and that confusion is used to discover what way is best to help that particular individual.

Different parts of the background material becomes motivated at different times within the course. It could help the students to provide a key from possible trouble spots to relevant background material.

\subsection{Example}
We use the model of students' conceptualizations shown in \ref{} to provide background material for a course in software engineering organized around the concept of provability-driven development.
Finding the calculational approach of Gries\cite{}, which provides relatively succinct proofs to match well with the phenomenography of Rota\cite{}, who found that short proofs were more beautiful and more memorable, we prefer this style.



\subsubsection{Symbolization}
From the range of conceptualizations, we choose to include symbolization, and formation of valid arguments stressing that rules of inference satisfy guards upon the transformations we can make as we transition from one statement to another.

\paragraph{Self-assessment Questions}
%if you do well on questions, you can skip to next
%symbols are used in Floyd-Hoare triples, so use them in self-assessment questions
Which of the following describes a while loop executing?\\
boolean done = false;\\
while (!done)\{\\
statements which eventually change done to true\}\\
\begin{itemize}
\item ($\neg$done)(statements)(done)
\item ($\neg$d)(statements)(d)
\item ($\neg$p)(statements)(p)
\item (p)(statements)($\neg$ p)
\item all of the above
\item none of the above
\end{itemize}

Which of the following describes two statements executing in sequence (where, for any $i$, $s_i$ denotes a state of the variables being used by the program)? Please note that reading the value of variables does not change the state.\\
\begin{itemize}
	\item (in state $s_0$) (print "Hello, world")(print x)(in state $s_0$)
    \item (in state $s_0$) (x=x+1)(print x)(in state $s_0$)
    \item (in state $s_0$) (x=x+1)(print x)(in state $s_1$)
    \item 1 and 3 but not 2
\end{itemize}

Please note that the questions have been designed to help you notice the content being explored. If you find that the phrasing of the questions is helping you arrive at the correct answer, you should choose to study the material.
\paragraph{Material}
Variables, which can be individual letters, or names, either in computer programs or in mathematical statements, are used to represent ideas.
In programs, meaningful variable names have been shown to increase the speed and correctness of comprehension.~\cite{}%teaching and learning formal methods
In mathematical statements, single letter variable names have been shown to improve the skill of abstraction.\cite{}

Thus we choose to employ meaningful variable names for now, but will tend to replace them with single letters later.

You have probably seen variables in high school algebra, for example in the equation for a line, typically written as $y=mx+b$.
Here, $y$, the vertical position on a graph, is calculated from $m$, the slope of the line, and $b$, the vertical offset when $x=0$.
A family of parallel lines can be generated by keeping one value for $m$, and setting different values for $b$. Thus we see that a variable can refer to a single value, and a variable can also refer to different single values at a time. For any one point along a line, when the value of $x$ refers to a single value, the single values of $x,m$ and $b$ can be used to calculate a single value for $y$.
It is, however, also possible to think of the values of horizontal axis all together, and refer to that idea by a single variable $x$.

If you are familiar with a program language, such as MATLAB, that supports vector variables, you will have seen single variables that can refer to many individual values at once. Likewise, you may have worked with arrays of one or more dimensions; reflecting on this, the array name (without specified indices) can be thought of as referring to the entire array.

Keeping that idea in mind, we can contemplate the mathematical expression $0 \leq x \leq 1$. When $x$ is an integer, we have that the integers 0 and 1 satisfy this description. Depending upon context, $x$ may represent the range including these. Changing the universe of discourse from integers to reals, the expression $x <3$ represents, depending upon context, not necessarily only a single, yet-to-be-determined real number that also has the property of being less than 3, but also it can be that $x$ represents all real numbers less than 3.

\subsection{Logical Operators}
We wish students to understand  strengthening and weakening of conditions.\\
We wish students to understand the idea of a precondition as a disclaimer, and also as a guard.\\
We wish students to be able to negate statements with multiple quantifiers.\\
We have seen from investigating the conceptualizations that students can have trouble even negating statements with single quantifiers.\\

\subsection{Relations}
We want students to understand relations, because we want them to see the pairing of an input state and an output state, as a result of a transformation by a computation, as a relation.


\subsection{Rules of Inference}
Calculational proofs \cite{Gries} %in TLFM
seem to suggest strongly the way to proceed.\\
Stepping through examples of these might help students comprehend


\subsection{Internalization and Interiorization}
Recall that internalization has been achieved when a student can perform a process correctly, not necessarily recognizing the circumstances in which that process is appropriate. 
What distinguishes interiorization from internalization is that the student can examine and discuss the process, beyond being able to carry it out. 
It is important for the software engineering course that students can examine and discuss the process of program derivation from requirements. Recognition of the circumstances in which automatic program derivation can be performed is an important part of understanding requirements.
We combine internalization and interiorization because our interviews have not addressed topics that the participants cannot discuss.
We have however found student testimony that processes that can be carried out confidently are not used due to lack of a means to determine whether the process is appropriate to circumstances.

\paragraph{Self-assessment Questions}
Which, if any, of the requirements described below can be satisfied by a finite state machine?
\begin{itemize}
	\item Recognize whether or not a string could have been generated by a regular expression
	\item Recognize whether or not a string could have been generated by at least one of a set of regular expressions
	\item Recognize whether or not a string could have been generated by juxtaposition of strings, each of which could have been generated by at least one of a set of regular expressions
	\item all of the above
	\item none of the above
\end{itemize}

Is this a mapping from a recursive algorithm to a proof by mathematical induction?\\
 The base case or cases of the recursive definition map to the base case or cases of the proof, and the recursive call or calls of the recursive algorithm map to the induction step. The recursive call or calls are always invoking with a problem of a smaller size, and the inductive step is always working with a premise that is assumed to be true. In both recursive algorithms and inductive steps, the next problem is solved making use of a previous solution.

Is this a mapping from a concrete example of a proof to a proof in a more abstract circumstance?\\
Concrete\\
There is a commercially available car, a deLorean.\\
There is an unreachable goal, time-travel.\\
Spielberg has shown us that if only we had a "flux-capacitor" to attach to the deLorean, we could have time-travel.\\
Therefore we conclude that the flux-capacitor must also be unreachable, by the following logic:\\
If we had the flux-capacitor and the deLorean, we would get time travel.\\
We cannot get time-travel.\\
So, we cannot have the flux-capacitor and the deLorean.\\
We can get the deLorean.\\
So, it must be that we cannot get the flux-capacitor.

Relatively Abstract\\
There is a simple algorithm, $M$, by which we can determine whether two finite sets have any elements in common.\\
There is an unreachable goal, $A_{TM}$.\\
Sipser has shown us that, if only we had $E_{TM}$ and the above simple algorithm, we could have $A_{TM}$.\\
We cannot get $A_{TM}$.\\
So, we cannot have $E_{TM}$ and the above simple algorithm.\\
We can have the simple algorithm,$M$.\\
So, it must be that we cannot get $E_{TM}$.

In symbols:\\
$\neg A_{TM}$\\
$M \land E_{TM} \rightarrow A_{TM}$\\
$\neg A_{TM} \rightarrow \neg (M \land E_{TM})$\\
$\neg (M \land E_{TM})$\\
$\neg M \lor \neg E_{TM}$\\
$M$\\
$\neg E_{TM}$




\paragraph{Material}


\subsection{Perceptual}
\paragraph{Self-assessment Questions}

\paragraph{Material}

\subsection{Transformational}
\paragraph{Self-assessment Questions}
		
\paragraph{Material}
		
\subsection{Axiomatic}
\paragraph{Self-assessment Questions}

\paragraph{Material}
To detect 

\section{What Do You Say After You Say HelloWorld?}
This is a software engineering course, organized around the idea of provability driven development.
We want to impart the desire to approach software engineering problems with
methods of formalizing
calculation
checking
\subsection{Math for Proof}
Mathematics provides what is necessary for proofs, by means that include precise definitions.
We would write definitions of program function in  a style admitting proof.
We will use finite automata.
So, a section on proof, followed by a section on finite automata, formal definitions of things we use, clients, servers, files, streams,
\subsection{Proof of what}
What sort of things are we aiming to prove? liveness, safety, accuracy,
i/o relations for component based systems
resource utilization including time
utility functions
\subsection{Autogenerated Code, Proof by Construction}
The construction technique  needs to be proven.
BL, statecharts, Wise computing
\subsection{Levels of Abstraction}
This goes with composition of system.
Unlike Wing, we do not pick one, rather we relate (multiple possibilities to one another?) them, like ISO standard communication stack
and those defined things live in the space of abstractions
so, make the space from the defined things, and situate the defined things in the space
invariant as an example of abstraction, i.e., many different operational sequences covered by one invariant
\subsection{Types, Systems of Types, Operations}
What impact does provability have on these?
structure in types
data structures meets provability
(reursive data structures, proof by induction)
can we represent data structures as finite automata?
Is there a reason why not to do this, e.g., would it not be sufficiently general?
representing datatypes with algebras
Hoare 1985
Milner 1980
\subsection{Definition, Denotation, Operational, Axiomatic}
models, with math, might have more properties that we want to use, vs.\\
theories, with which we create only our desired properties.\\
Z, VDM, emphasize models over theories
\subsection{Formal Methods}
Z VDM, Larch
algebraic specification language
would we want to use Tempo instead of OBJ?
A formal method has an assertion language, for example, 1st order predicate logic
A formal method has a specification language, which in turn has a syntax and a semantics.
The syntax contains rules for formulating syntactically correct (legal) terms

\bibliographystyle{alpha}
\bibliography{literature}

\end{document}