DFSA

DFSA or Deterministic Finite State Automaton is  a way to tell machine to react with particular input. Coming up an DFSA is quite easy but at the same time it can be challenging if more than one requirement is need to be fulfilled. Hence, there is certain tactics that we can use to create a DFSA.

First of all, if there is more than one condition need to be fulfilled, then create different DFSA for each condition, then try to combine both of the DFSA to come out with new DFSA which will match both requirement.

In order to prove the DFSA, we need to first generate a transition function for the diagram that we build. Then from that transition function we can come out with a extended transition matrix, which will describe each state of DFSA. This is a good way to know whether our DFSA will work for all inputs and outputs. 

Algorithm and it's proof.

Coming up an algorithm is hard enough and proving that it works is even harder. To prove algorithm, there is certain steps that we have to follow:

               1. Determine Pre-condition.

                              Pre- conditions are the requirement that we impose, so that our algorithm can work.                Pre-condition must be reasonable and doesn't directly related to post-condition.

              

               2. Determine Post-condition.

                              Post-condition is the output that we want from this code, not only for the return value                but we also can set post-condition for each variable that the code uses.

               3. Come out with Induction Hypothesis

                              One of the hardest thing in the proof is coming out with an IH. The IH must combine                pre-condition to post-condition.

               4. Proof by induction.

If all the 4 steps are followed correctly, then most probably we can proof the algorithm. However, the last step is very important and quite hard.

Proofing Iteration.

Proving iteration might follow the same steps but before coming up with IH, we need to identify our loop invariant. Loop invariant is the thing that does not change during iteration. The loop invariant is very useful when proving the loop as well as when proving that the loop will end. In order to prove the iteration, it's better to split the proof into two proof.

               Partial Proof:

                              Prove that the loop will satisfies post condition if the loop terminates.

              

               Termination Proof :

                              Prove that the loop will terminate.