ch10.tex

\chapter{Future Work}
Neuroscience ( and some study in software engineering) leads to believe helping students pay attention and remember intrinsic reward, the sense of pleasantness, helps students remember Make use of the natural experiment --- some students will have enjoyed the material. Are these the ones who remember better? and does the nature of enjoyment make any difference in understanding productivity aesthetics?
\section{Helping Students Discern Derivation for Proof of Correctness}
Recall that variation theory holds that students cannot discern a thinkg unless contrast is provided.
Pang has pointed out that, for persons aware of only one language, ``speaking'' and ``speaking their language'' are conflated.
Only when the existence of a second language is known, does the idea of speaking become separated from the ide of speaking a specific language.
We may wish to alert students to the ability to derive code from requirements mathematically.
We could show them, for example, an even function.
We could show them how to construct a function that is even.
We could show them how to construct a function that is odd.
This might hep them see the difference between writing code and testing it afterwards, and deriving the code to be correct by construction.


Variation theory and cognitive science suggest the teacher should make an effort to show positive and negative examples and to point out what causes one to be positive and the other negative to help discern the relevant features. Have you noticed this practice? Did you find it helpful?\\

Engagement with the material\\
Please rank order the factors that might help you e engaged wit theh material\\
job related\\
prereque\\
have been curious about\\
fun\\
competition\\
beautiful\\
(Does this happen often)\\
(Does this matter to you?)\\
What, if anything, makes you engage with the material?\\
 Neurophysiology suggest that animation in overheads makes it easier to be alert to material, that figures draw attention more easily than text.
 Plesae comment on what if any things make animation helpful to you, or whether you find some animation helpful.
 If you find figures helpful, can you comment on how they help? Do you find it easier to pay attention to figures than to text?

\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 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 have an idea which mathematical tools we wish to use, and on
the other hand we have an idea 
of the extent of the students' conceptualization.
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 rigorous description of these processes.
Path algebra out to be accessible to the students.
We could introduce (typed) lambda 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.
Having the use of typed lambda calculus for path algebra, we can then use it to describe the effect of instruction in the context of Floyd-Hoare triples.
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{User of Bridging Material}
The material on mathematical tools we wish to use should be introduced at a level that addresses the 
conceptualizations 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 poing 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 make evident the 
critical aspects, that distinguish on 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 become 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  () 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, matching well with the phenomenology of Rota, who found that short proofs were more beautiful and more memorable, we prefer this style.
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.
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$)(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 variable 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. Variables, which can be individual letters, or names, either in computer programs or mathematical statements, are used to represent ideas. In programs, meaningful
variable names have been shown to increase the speed and correctness of comprehension \cite{} In mathematical statements, single letter variable names have been shown to improve the skill of abstraction.
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 programming language, such as MATLAB\textregistered, that supports vector variables, you will have seen single variable that can refer to many individual values at once.
Likewise, you may have worked with arrays of one ore more dimensions; reflecting on this, the array name (without specified indices) can be though 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 student 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{are these Gries?} 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 process that can be carried out confidently are nevertheless not used due to lack of a means to determine whether the process is appropriate to circumstances.
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 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 ddLorean.\\
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 $M$, we could have $A_{TM}$.\\
We cannot get $A_{TM}$.\\
So, we cannot have $E_{TM}$ together with $M$.\\
We can have $M$.\\
So, it must be that we cannot get $E_{TM}$.\\
(I'm thinking pictures would help.)
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}$

\subsection{Perceptual}
\subsection{Transformational}
\subsection{Axiomatic}
To detect
\subsection{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.
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, 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.
The construction technique needs to be proven.
BL, statecharts, Wise computing This goes with composition of systems.
Unlink (in a book on formal methods)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, i.e., many different operational sequences covered by one invariant.
What impact does provability have on these?
structure in types data structures meets provability (recursive data structure, 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 models, \cite{milner1978theory} 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,
Z VDM Larch algebraic specification language would we want to use Tempo instead of OBJ?
A formal method has an assertion language, for example, first order predicate logic.
A formal method has a specification language, wich in turn has a syntax and a semantics.
The syntax contains rules for formulating syntactically correct (legal) terms.

Mitchell \cite[p. 35] (Foundation of Programming Languages) says Hilbert-style proofs system consists of axioms and proof rules.
axiom provable be definition\\
a proof is a structured object build from formulae, according to constraints established by a set of axioms and rules of inference.

Arcavi et al.\cite[p. 56]{arcavi1998teaching}''Work in cognitive science\cite{mcleod1992research} has shown that students' beliefs about the nature of a subject may have profound effects on their learning of it % (McLeod 1992) Research of affect in mathmatics education: A reconceptualization In Doublas A. Grouws (Ed.) Handbook of research on mathematics teaching and learning [pp. 575-596 NY Macmillan]

One approach to teaching students to generalize is used by Schoenfeld (page 60 and earlier), who teaches his students heuristics, including one from Polya, about problems with fewer requirements 

Researchers have noticed that students, having learned procedures, have not necessarily learned to apply them. 
Cipra 1995 UME Trends The bumpy road to reform 
Culotta 1992 The calculus of education reform science 255