The introductory video, available here (as "cse331-24su-intro" and slides here), included some background material on the software development process, i.e., the steps we go through from receiving a description of code to write and pushing it to end users. That material is background for all of the topics discussed below.
An introduction to writing code that runs in the browser. We will discuss the environment in which our code is run and the languages that we will use, JavaScript and TypeScript. We do not assume any prior knowledge of either language.
You may find that the second language you learn is actually the hardest! This can be because some things you took for granted in the first language are not the case in the second language. That can be unsettling, like the ground is shifting under your feet. In response, you feel like you need to look carefully at your feet as you take each step.... But that is exactly what we want for this course. We want to revisit core aspects of programming languages and make sure we have a complete understanding of how they work, what mistakes are possible and impossible. Having seen two languages, Java and TypeScript, will also help us understand the range of possibilities for what languages can do for us.
The introductory video noted that three principle techniques are used in practice to ensure that the programs we release to users are bug-free. These are testing, tools, and reasoning. In this topic, we will see that, while all three techniques are almost always needed, the amount of each needed depends on how complex the code is. We break this into levels of difficulty based on the language features used.
We will, then, go into detail on the first two of those techniques: testing and tools. The remaining topics in the course will go into detail on the third and most important technique, reasoning.
Before we can apply correctness techniques at all, however, we must first know what the correct output should be, which is given to us by a specification. Since getting the details right is critical here, we will introduce a formal language to use for writing precise specifications.
In this topic, we begin learning about the most important tool for ensuring correctness: reasoning, which means thinking through what your code does to convince yourself that it is correct. Unlike testing, reasoning checks the correctness of all inputs, and unlike the type checker, reasoning ensures that the outputs are exactly what is required, not simply in the right set of values (the type).
Reasoning can be done formally or informally. Most professionals reason informally, in their heads. In class, we will learn formal reasoning because (1) it is much more teachable, (2) it contains key ideas needed for informal reasoning, and (3) it is required in practice for the hardest problems.
This week, we will start with the simplest case, which is reasoning about straight-line code without mutation. In the remaining topics, we will learn to reason about code that is not straight-line and then code that contains increasingly complex types of mutation.
index.tsx.This week, we continue to learn how to reason about code without mutation by moving on to code that involves recursion. Reasoning about recursion requires a new tool called structural induction. With that tool in hand, though, we have everything we need to handle any code that does not mutate.
crazy-caps-decode to be
"returns a list of the same length but with every three character,
starting with the third, made lower case" instead of "...starting with the
second..."worm-latin-encode example to be "kevin" becomes
evinkorm" instead of "Kevin"...In this topic, we will finally begin to mutate local variables. Unfortunately, this substantially complicates reasoning about the code, requiring an entirely new set of tools called Floyd Logic. Fortunately, we will also see that there are additional tools, called forward and backward reasoning, that can mechanically translate complicated reasoning problems in Floyd Logic back into ones that our earlier tools are already capable of handling.