What is the difference between static and dynamic world views.
Static means that something is not changing over time and dynamic means that it is changing over time. When you don't care (or specify) how something gets from one state to another, you are taking a static view. When you describe step by step how the state transition occurs, you are taking a dynamic view.
In the static view of mathematics, like in our MIS, we specify how variables change by stating their value or properties of their values. For instance we might specify that we take a sequence s and return the maximum value of that sequence. We do not care what algorithm is used to find the maximum, only that it has the property that it is greater than or equal to all other values in the sequence.
In an imperative programming language like Java we give all of the steps for a state transition. We give the algorithm, like explicitly looping through all of the elements of a list searching for the maximum.
A functional programming language does not give instructions, instead it defines functions, which are a mathematical concept. You do not worry about the steps in an algorithm. To calculate the maximum of a list, a function is defined recursively. The edge condition is the maximum of a singleton list, which is equal to the only element in the list. The recursive case is the maximum of a longer list, which is the head of the list if the head is bigger than the maximum of the tail. If the maximum of the tail is larger, then the maximum is the maximum of the tail. Code for this, and a further explanation is available at:
http://learnyouahaskell.com/recursion
I can see why FSMs are confusing, since they do capture something about change. For a simple FSM the code and the mathematical specification will look almost the same. In a case like this, the mathematics has also taken a dynamic view. However, for more complex FSMs, like our Module State Machine, the specified state transitions abstract away details. The algorithm is missing, so in this sense they are again taking a static view.
Testing is considered a dynamic verification technique, because it involves running the program and all of the associated changes of state through the execution of the algorithms. A mathematical correctness proof is static because the code is not run, which means no algorithms are executed.
