DFSA

In some degree, the most challenging question in assignment 3 may be the last one.
I once got stuck on combing the two machines representing binary string with odd length and multiple of five respectively. I wasn't sure what were the exact steps using cartesian product. So i considered all the combinations of the cases of the third machine i want to construct.
That is exactly the result of cartesian product. Excluding the initial state, there are 5*2 = 10 states
for x = n mod 5 with odd/even length. These are the state invariants. Then We can see directly from some binary numbers and derive the transitions. Then the desired machine is fulfilled.
The proof of a DFA is straightforward. For me it is kind of a process of verifying each state go to the correct place via a path or an edge. Graphically, each state is a node with inputs and outputs.
Thus the transitions explain the correctness of traversals in a machine.

review of Week 10

The annoying assignments, exercises, quizzes and term tests seem to be paused except for CSC236. This weekend i have to engage into the second last assignment with my partner. I also have a somehow big project of csc207 to worry about. Insipte of the workload of a computer science student, i now write for my 6%~11% of the final mark.
These two week we saw pretty much things about finite state automata and regular expressions. Regular expression is a descriptive way to express the language. We can design our own language with different alphabet using regular expressions. Through the example in the lecture, such as an alphabet of binary numbers containing even or odd zeros, i learned a logical procedure to analyze the syntax between various languages. The interesting part for me is the algebra on regexes. Without changing the language, one can apply some principles such as: commutativity, distributivity to the regular expressions. This simplifying process allows more variations on a language and it provides some interesting design patterns of a language.
Another thing is the DFA, or DFSA. The first time i saw it was in CSC148 when we were doing the graph algorithm. It seems there is quite a few connection from the DFA to graph algorithm. Machines of DFA accept their unique pattern of strings. We can easily find out whether a string is valid to the machine by traversing between the states. The hard part is how we construct a desired machine for a particular collection of strings. By observing the pattern of some strings, we need to derive some crucial parts of the machine like the state invariants and the transition functions. A graph is usually helpful to verify the state the next character heads is correct, which is to say, we need to carefully set our initial state, final state, states between and all the edges. Such things is really thoughtful.

After Test 2..

Since there is always a lot of people there in the day section, i wrote the night section test.
I don't know how big the difference between the day section and night section test. They may follow the same patter pretty much. I didn't work out satisfying answers on the test.
About the palindrome, i remembered well that i did the same thing in CSC108 lab. But one thing
to regret is that i forgot the prove structure. I tried using complete induction but i didn't organize the frame well.
Related to the last question in the test, i really got a mess in my mind during the test.
I got frustrated when i could not figure out right away the main purpose of the function downward(n). Things happened and i got all blank in my brain. When i got calm down and refreshed my mind, i tried out some typical examples. Unfortunatley, i didn't realize that the loop invairant was sth like the floor of lgn until hours after the test. Anyway i cannot say i fail the test, at least i failed getting an insight on the subtle things.

More on iteration

The 3-hour night version lecture is a real torture. For the example counter(m,n), i can't relate the loop invariant directly to the correctness of the program. It's weird that the b value is set to 6.
I tried pick two non-zeros natural numbers for m and n randomly. And the loop has to execute 6 more times to terminate after a and b decrease to 0 since b is assigned to 6 and c has to counter 6 more times. It may be necessary to use the loop invariant c = 7m + n to go to the postcondition, but it seems not to be that straightforward to be understood. Now i realize the importance of code design that make other people's life easier, for people who are learning how to prove loop invariant. Back to the loop invariant, i usually trace algorithm on simple example, like iterates for a few times and see what kind of changes are caused. As to me it's more helpful than just thinking of some fancy relationship between precondition and postcondition.
For more complicated loops, like nested loops, these things have to be done inside out. Prove termination and loop invariant in the very inside, then for any value of the loop outside, prove termination and loop invariant for outside loop. In the selection_sort example, the inside loop is going from index j=i+1 to the end of the list. Selection_sort is basically "selecting" a proper position for an element in the unsorted section of that list. I take a [4,2,3,1] as an example to run the loop. The inside loop actually helps me to evaluate a position by comparing the value of 4 to 2,3 and 1, then the outer loop moves to the next index and this easily sorts the whole list. But the inside loop may have k+1 iteration or may not. Since the value of the number could be equivalent. These "special" cases happened because of the postcondition, which is non-decreasing order here. Then it's not hard to prove the program "moves" and "compares" in some range.

Busy Week 8

A2 was submitted a few days ago, but i didn't work out the first problem, neither did my partner.
I didn't derive a valid recursive formula for the 3rd problem as well. So i just proved it without a valid formula, which might lose some marks probably.
Luckily the 207 midterm was over this afternoon, i now have more time to review the materials Danny had talked about iterative programs.
It's again easy to start with, and more interesting than the previous sections. Obviously, we will use a lot of simple induction stuff here, for proving correctness of iterative programs. It's tricky to seek for a proper loop invariant, and it always takes times to go through the loop and see how this 'incomplete solution' works. Again, to prove the correctness, we carefully trace the loop and the changes each time it caused. This helps us to fulfill the implication from the ith to the (i+1)th loop.

the end of week 7

Proving program correctness is always an annoying part, especially dealing with searching items and sorting items in an array or list. There are many conditions to consider for the program(most of them we have seen during this week were recursive programs) correctness.

The proof of correctness may be like: by induction, for size of the input,
prove precondition -> termination&postcondition. It seems the structure of
complete induction is well following recursive structure.

Then we go through the first few lines and if lucky enough we can proceed to the
annoying part of the recursive function. In this case, the recursive step leads us
to examine the whole function again with different input size, a smaller size.
We don't stop checking until we get the expected result - the post condition.
But how to split up the size so that it will look more straightforward and easier to
be checked? For the binary search, the way is to break into the middle of a list.
So there may be various ways and algorithms for various problems to shrink the
searching or sorting range. The next thing is to continue on executing. The case
must be carefully chosen otherwise some unexpected errors may cause the crush
of the program.

The proof is complicated at most of the time so as to ensure all the codes work from the
first line with the initial input. It saves us a lot of time to complement any cases or to fix
up any mistakes afterwards.

Lecture about Program Correctness

Monday came, Danny didn't come.
A lecturer named Nick presented us a lecture about program correctness.
Nick started by the sentence "My program is correct." He talked about how correct a program
would be from different points of view. He spent some minutes on explaining the definition of conditions, the relationship between precondition and input, postcondition and output.
This helps us to recall what we have learned in CSC165.
Then he gave the very familiar example, binary research, to reinforce the concept on how a program would be correct in each step. One question(maybe just for fun, maybe not) he mentioned during the lecture was 'how do you crush a program', which sounds very illegal.
But at the same time, this is just the way to prove the program correctness backwards.
I believe if one can crush a program easily, then it wouldn't be too hard to prove correctness.
That is where you see right from wrong. So yes, let's enjoy crushing our programs.