Smart Software

Lang.NET Presentation

I presented at both the Lang.NET Symposium and Seattle Code Camp, but it didn't proceed as I originally planned.

For several months, I have been changing the back end of my software to scale better and retain sufficient control of the performance of my product under all circumstances. I do have some hard-coded limits, but these limits and time constraints don't really work well the way my software is written. They are better for catching events that should never happen. The changes were extensive as I used functions pervasively to compress the size of my expressions and maintain the invariant that expression size stay proportional to program size. Manipulating arbitrary functions, particularly recursive functions, in a general and efficient way is really difficult.

I was using these two events as a forcing function for releasing my software. Unfortunately, I didn't make my deadline. I lost about several days of productivity due to a random apartment incident. I skipped a day and half of the conference to prepare in a valiant attempt to demo the most recent build of my software. Instead, I used an old release of my software from six months back, and messed up my demo since I forgot that I could only execute expression in the immediate window from within the context of an error.

My presentation relied heavily on slides rather than a live demo, which was not my plan. People want live code. Presentation slides also leave the audience confuse about the nature of the product as Ted Neward wrote in his Lang.NET review.

For people reading my blog, there wasn't too much extra information above and beyond what I have talked about in the past, since I could not assume that people were aware of my product. Some new points include the liveness of the environment, closed forms and some manipulations with functions.

I am wary about giving too much information, since I have leaked so much already for a considerable period of time without actually releasing the product.

I prepared the slide a month in advance, hoping that I would make changes over the course of the month, but ended up spending a full day polishing the presentation before my Code Camp talk.

Some reactions:

• Four Microsoft researchers quizzed me.
• A number of people that I have met read my blog... Most of the Microsoftees appeared to be familiar with me.
• A few people asked how they could apply for the beta. Others were hoping for a Java version. Miguel comment to me that it was a great presentation. I was surprise of my healthy applause, because I hadn't been paying attention and have never given any applause. The applause level was similar to Miguel's presentation later on, so I couldn't actually tell if the applause was enthusiastic or ordinary.
• Some questions on technical aspects:
  • did I utilize an available prover software like Z3? I wrote the software myself.
  • has my prover been benchmarked? No, and it's doesn't deal with the types of formulas use in the benchmarks.
  • how do I handle complicated cases like overflow. My overflow checking is very limited, since, in the past, I wasn't interested in cluttering my assumptions, but adding such support is trivial and now also less problematic.
  • how do I deal with invoking function variables (ie, delegates). I represent them exactly, but, for the sake of analysis, I ignore the potential effect on state if the function is unknown.

Postmortem:

• Create setup files regularly. Though I update component libraries frequently, I relied too much on .NET's XCopy support. Despite having copy DLLs to output folder, I was not able to get the build that I want working.
• Save interesting snapshot pictures of the product while in development. I reused a lot of images from my blog.
• Always try to have a working build. Include notes about the status of the software. I took a random setup build without remembering what state it was in.
• Conversations and event draw energy away from me. I usually enjoy my energy juices and bars before development, but I should actually remember to do even more so before presentations.
• Get well-rested before a presentation. This is unusually difficult for me, because I work during nights and sleep during the day.

There is still a geek dinner coming up in the next week that I may take advantage of to give a live demonstration.

Playing Chess with God

Although the title is appropriate, I wasn't actually planning on writing a post about the legendary chess grandmaster, Bobby Fischer, who died in the past few days, but I will take a few moments to pay my respects.

I was a long admirer of him, and, over the years, I identified with him ever more over the years. Here was this young natural talent who defeated several highly trained Soviet chessplayers to end Soviet domination of the chess world title. He was also very individualistic, provocative and controversial, breaking taboos and openly defying the government, by traveling to Serbia despite sanctions. In the same vein now, I do fancy myself competing against other companies and speaking freely.

Back to my intended post, I found this interesting post called "Play Chess with God" by an interesting new blogger, Russ Cox. This and his other post, SuperOptimizer, deals with computer solutions to traditional human problems mainly through brute force techniques.

Starting in the late 1970s, Ken Thompson proved by example that computers could completely analyze chess endgames, which involve only a small number of pieces. Thompson's key insight was that when there are only a few pieces on the board, there might be very many possible move sequences, but there are relatively few distinct board positions.

Given six pieces in the board, it became a simple lookup with Ken's endgame database to determine the best next move to make. Russ quotes former championship chess player Tim Krabbe describing his experiences using said database:

Playing over these moves is an eerie experience. They are not human; a grandmaster does not understand them any better than someone who has learned chess yesterday. The knights jump, the kings orbit, the sun goes down, and every move is the truth. It's like being revealed the Meaning of Life, but it's in Estonian.

While my software relies more on intelligent rules rather than brute-force techniques, the feelings and experience that I have experienced are more or less the same. My initial thought sometimes on seeing a strange result calculated by my NStatic tool is denial with the full belief that I am witnessing a software bug, only to discover after careful analysis and to my surprise that the computer's solution is in fact correct.

I don't claim this experience to be unique. This should be familiar to anyone who has ever played chess against the computer or used a declarative programming language with unpredictable control flow.

Human-like Reasoning

My goal in my static analysis work is not to solve general problems like the Four Color Theorem, but rather to simulate closely the human reasoning process to solve problems that are generated, comprehendible, and solvable by normal people. Practical and deep, rather than complete.

Humans write programs to be understood by other humans. Human understanding comes about instantaneously or with relatively little effort compared to the work performed by many analysis tools. We typically don't unroll loops and recursion, but instead "get" the meaning of programs by recognizing a few standard patterns. We look at a program and instantly see a sorting operation taking place, for instance. Programs typically consist of these recurring patterns. In many programs, the only complex data structures used are a standard few like arrays, hashtables, linked lists and stacks. My approach to reasoning adheres closely to the way humans think, even when more efficient computational approaches exist, so as to align my software with human performance; the one exception is when non-human-like approach is strictly better in every way, yet yields identical results.

Stephen Wolfram, inventor of Mathematica, wrote a post Mathematics, Mathematica and Uncertainty touching on some of these themes. Even with the more advanced symbolic capabilities of Mathematica--virtually infinite compared to more than my own software package, Wolfram encountered limits trying to use his own system to verify itself.

Sometimes we use the symbolic capabilities of Mathematica to analyze the raw code of Mathematica. But pretty quickly we tend to run right up against undecidability: there's a theoretical limit to what we can automatically verify.

Yet, I think that our approaches deviate somewhat in that Mathematica isn't geared to testing programs. Also, the Mathematica code base is not typical. Being a program for doing mathematics, it naturally consists of advanced mathematics, difficult for mortals to understand and involving non-linear arithmetic, which is theoretically undecidable.

The code was pretty clean. But it was mathematically very sophisticated. And only a very small number of experts (quite a few of whom had actually worked on the code for us) could understand it.

Another point that Wolfram makes is that, contrary to my approach, Mathematica typically avoids imitating humans but instead uses complicated, non-human-friendly procedures extending hundreds of pages in length, roughly the size of the entire analysis portion of my code base.

Think of almost any mathematical operation. Multiplying numbers. Factoring polynomials. Doing integrals. There are traditional human algorithms for doing these things.

And if the code of Mathematica just used those algorithms, it'd probably be quite easy to read. But it'd also be really slow, and fragile.

And in fact one of the things that's happened in Mathematica over the past decade or so is that almost all its internal algorithms have become very broad "polyalgorithms"---with lots of separate algorithms automatically being selected when they're needed. And routinely making use of algorithms from very different parts of the system.

So even if there's some algorithm for doing something that's written out as a page of pseudocode in a paper or a book, the chances are that the real production algorithm in Mathematica is hundreds of pages long---and makes use of perhaps hundreds of other sophisticated algorithms in other parts of the system.

But such algorithms were not constructed to be understandable---and much like things we see in physics or biology, we can see that they work efficiently, but they're really difficult for us humans to understand.

And in general, the way Mathematica works inside just isn't very "human friendly"... Like when Mathematica does an integral. It doesn't use all those little tricks people learn in calculus classes. It uses very systematic and powerful methods that involve elaborate higher mathematics.

Supercompilation

I noticed work by SuperCompilers, LLC on supercompilation that takes on the myth of the sufficiently smart compiler (which I previously wrote in my post on Humans vs Computers). Their technology seems very similar to my work with its reliance on partial evaluation.

The company deals with the same sort of criticisms about NP-completeness and undecidability in their white paper "Supercompiling Java Programs."

The problem of fully optimizing an arbitrary computer program, when mathematically formalized, turns out be an incomputable problem, we do not need to optimize arbitrary mathematically given computer programs, we only need to optimize programs written by humans. And humanly-written programs tend to have a lot of special structure too them, including both obvious and subtle redundancies that lead to inefficiencies.(this is related to algorithmic information theory; see, Chaitin, 1987 and Bennett, 1986). There is no possibility of ever creating an algorithm that can fully optimize a general computer program. Fortunately, though, the practical problem of program optimization -- though still very difficult -- is a lot easier than the general mathematical problem to which it corresponds. Because, in reality

Supercompilation does not try to solve the impossibly hard problem of fully optimizing an arbitrary computer program. Rather, it is an extremely valuable heuristic technique, which seeks to find ways of significantly optimizing a wide variety of computer programs. Most real-world computer programs are chock full of inefficiencies, which can be removed via the supercompilation process. These inefficiencies are often hard to see in the source code, but they are highly transparent when the code is translated into a more mathematical form, as is done inside the supercompiler. Some of these inefficiencies are introduced by sloppy programming; others are placed there intentionally, by programmers interested in goals besides efficiency, such as maintainability and comprehensibility of code, or speed of software development. In many cases the most efficient way to implement a given piece of code is a truly humanly infeasible way, involving literally hundreds of times more lines of code than the ways that occur naturally to humans.

Another post "Illogical Arguments in the Name of Alan Turing" in O'Reilly's website criticizes bad arguments by people, that static code analyzers are not useful at all because they are limited by the halting problem, or that logic flags can never be found because of the halting problem.

Humans are subject to the same theoretical constraints as computers, but yet they do not perform the same laborious, brute-force search. Instead, humans employ a strategy of recursive pattern matching and replacement when thinking about and checking their programs. The kinds of programs that people write are those that they can easily reason about and review later; being maintainable, these programs belong to small subset of possible programs and are inherently tractable for analysis.

One paper "Solving difficult SAT instances in the presence of symmetry" suggests that the structure of a problem can affect its performance. That, in practice, a technique such as SAT-solving which is known to be NP-complete, often doesn't break down as it theoretically should. The authors point to the presence of large number of symmetries in the problem as somewhat of a requirement for explosive behavior.

Research in algorithms for Boolean satisfiability and their implementations [23, 6] has recently outpaced benchmarking efforts. Most of the classic DIMACS benchmarks [10] can be solved in seconds on commodity PCs. More recent benchmarks take longer to solve because of their large size, but are still solved in minutes [25]. Yet, small and difficult SAT instances must exist because Boolean satisfiability is NP-complete.

A 1994 Infoworld article quoted a researcher saying that deep static analysis requires years of analysis time. Upon reading that quote, I immediately thought that the researcher's approach might be very inefficient, because it implied that, after some depth, a human could outperform a computer on the same job. Perhaps, if we mimicked actual human reasoning, we could produce more effective tools.

Specifications

My main tasks in the past couple of months have been divided between bug-fixing and improving scalability. In the latter case, testing on large projects revealed bottlenecks caused by uncontrolled expression growth, for which I came up with a general solution. I have been spending a considerable amount of time on my simplifier for recursive lambda expressions.

There was one major addition. I added syntax support and highlighting for eventual specification support. My immediate goal was to provide a clean way of adding breakpoints and assertions to the source code.

The above visual shows what the new syntax highlighting looks like. The new keywords are bolded. Two new grayed out comment delimiters were added: //@ and /*@. These comment delimiters act like white space from within NStatic with the exception that new keywords are only recognized within the comments.

Any arbitrary code, such as ghost fields, can be placed inside these comments; this serves as an alternative to using the preprocessor defines, NSTATIC and CODEANALYSIS.

The new keywords that I have included: require, ensure, assert, assume, pure, modifies, invariant, old, breakpoint, result, unreachable, and nonnull. But, for the first release, the only keywords that are actually effective are assert, assume, breakpoint, old. Assert actually verifies that the expression is true and returns a warning otherwise (or error in the case of an invalid code path). The behavior is stronger than a call to Debug.Assert. Assume does not require the expression reduce directly to a true value, but it will produce a error if there is a false path leading to it.

The specifications are modeled on both Java Modeling Language (JML) and Spec#. There are quite a number of differences between the two. For instance, JML incorporates method contracts before the method declaration whereas Spec# incorporates contracts just right before the method block. While I followed the Spec# in this case, my instinct is to prefer JML, because it is more of an industry standard, and I am less likely to encounter Microsoft IP issues.

I suspect highly that the next version of C# will incorporate some kind of design by contract.

There are a few differences from both JML and Spec#.

• Arbitrary functions are supported as expressions with specifications, including impure functions (functions containing side-effects). Side effects that occur inside the expression of a single specification are not visible to other parts of the program, including adjacent specifications.

I have never taken a course in formal methods, so I am not fully aware of the implications of my approach.

Scalability

I wrote my NStatic tool to perform quickly with the goal of scaling linearly with the size of the code base. Analysis of a single terminal function is done in a single pass and is basically linear with the size of a function. Performance is impacted more by the call depth of some of the functions than by the number of functions in the code base.  Even with deep calls, I found ways of keeping analysis tractable through lazy and cached evaluations.

The main issues I am currently grappling with are some scalability issues that I discovered while scanning Rotor (the Shared Source Common Language Implementation). I found some interesting errors in Rotors, which I'll eventually post in my blog.

I also found some gotchas as well. My tool zipped through hundreds of functions in a split second before stalling in a function, which wasn't all that complex. Some of my transformations, while seemingly simple, exhibit exponential characteristics. This occurs when a function application duplicates an argument.

f(x) => x op x

Repeated forward use of such transformations can lead to large expressions that take long to evaluate or even print.

I found a general, elegant solution that I have been implementing. Ideally, the normal form should be at least as compact as the original form [considering the fully expanded lambda expression representation of f], preferably more so. With constant and atomic arguments, this is the case. For more complex arguments, the reverse transformation is applied: The left hand side of the transform becomes the normal form. It's counterintuitive, but there's no reason why we can't continue to simplify this normal form as the two sides of the equation have the same value.

VB & Other .NET Languages

Send me mail if you are interested in beta testing experimental Visual Basic or IL+PDB support (for other .NET languages including C++/CLR--please specify language) if and when I do include it in an NStatic beta. I don't know if I'll be able to handle DLR-based languages.

There's a slight chance for support of other languages in the beta, but it will be experimental and the primary focus is C#. Any other language support will come in a minor update. I don't have much experience working with other CLR languages other than C#.

If VB support is introduced, it will likely have rich editor and intellisense, but some parts of the analysis may exhibit C# semantics except when performing the analysis indirectly through IL. All other languages will have error highlighting support.

Omniscient Debugging

Bill Lewis of Tufts University, who is a computer scientist who has worked on natural language processing, gave a fascinating Google TechTalks lecture on "Debugging Back in Time." He also has a page dedicated to this new idea of Omniscient Debugging, where the debugger knows everything.

The omniscient debugger records every state change in the entire run of the program. Bill states that omniscient debugging gives the programmer a unique view of the program that eliminates the worst aspects of breakpoints:

• No guessing where to put breakpoints
• No extra steps to debugging
• Set breapoints, start, examine, continue
• No fatal mistakes... (no, "Whoops, I went too far")
• No non-deterministic problems
• Customers can email a debugging session to developers

An omniscient debugger can be extremely effective in understanding and fixing bugs. Bill's description and walkthrough of his prototype omniscient debugger (which in his words is more already more effective than any commercial debugger) seems to offer a genuine "silver bullet" approach to debugging.

His approach to omniscient debugging logs every state change to the program. This has the obvious disadvantage of slowing down execution runs and consuming disk space. Bill claims to have a found a practical way of doing this. The disadvantages are similar to those a profiler, but even more so, because each state change is logged, not just function calls.

I noticed a long time ago that my own analysis tool, which uses a completely symbolic representation of a program's abstract state space, could in theory be able to recreate the entire run of a program with just a compact set of critical assumptions.

This could be even more effective than logging, because of the superior time and space savings of my approach. NStatic can execute a long series of nested lengthy loops in less than a millisecond; it can allocate a gigabyte-size array and fill it up with values from any algorithm, and it would still take just the few K of memory that is needed to represent the algorithm itself.

There might even be some benefit to combining my "symbolic" debugger with Mike Stall's C#/IL managed debugger sample, so that I can retroactively incorporate symbolic reasoning to an actual just-in-time debugging session. One developer actually created Deblector, which uses Reflector to decompiling and debugging IL on the fly.

I did consider at one time being able to step forward and backward through the execution history. In NStatic Directions, I did mentioned making static analysis more into a debugger than a static analysis tool.

Making C# feel more like a dynamic, interpreted, REPL language through the use of a symbolic interpreter. Code is always live and can be statically debugged. As Erik states, programming will “shake of the yoke of the dreaded (edit, compile, run, debug)* loop and replace it with a lightweight (edit=compile=run=debug) experience.”

NStatic does already feel like a debugger with ability to watch and execute code immediately, as well as the ability to apply new assumptions.

Methods, Part 1

Method handling is difficult in static analysis. I will describe in a few parts some of the issues that I have had to deal with.

I demonstrated in earlier posts my handling of recursive functions in Loops, Part 1. In this post, I will show how I elegantly handle virtual functions. Below is the code for three classes, a base class Animal and two derived classes, Cat and Dog. Animal is an abstract base class, so no implementation actually exists for one of its member function.

Each animal can make a noise and has a type.

To test the three Animal classes, a wrote the following test method below. We have three variables of type Animal, "spot," "polly," and "tabby." We know Spot is a dog through an Assert statement. We know Tabby is a cat because we just created one from scratch. However, Polly is an unknown and sounds as if it may be a parrot, a class that we actually haven't account for; or, we could be mistaken, and it could actually be a dog or cat. 

So, I run the code through NStatic and extract out all the local variables and its member variables after the scan. Here's what the resulting Locals window looks like.

Whether we assign a variable or assume it, we know through the variables of the form "isXaY" that Spot is a dog and not a cat, and Tabby is a cat and not a dog. We also know that Spot says "Bark" and Tabby saw "Meow." We can also tell each animal's type from Animal's virtual property, Type. However, the Polly variable is mysterious. Thus, the local window has to represent all information about Polly's nature and behavior through conditional expressions and possibly generated values (in the case of Animal.Say(), which has no implementation).

 

NStatic Usability

I have invested the past three weeks into the NStatic user interface, polishing it up and considering how it will eventually be used. I didn't feel that the previous user interface was acceptable.

I'll take it to beta when it feels just right; I don't think it make sense to do it when there are still bugs that I am aware of.

I have given thought to the many different areas of the product:

• Interactivity. The performance of the tool is such that it is possible to interactively modify state and execute code in the context of the error. Much of the tool such as the intellisense, the class view, the error window, and file structure view are already synchronized in real time with text editor. The error window actually incorporates syntax errors dynamically as code as being edited.
• Manipulating and viewing the data. I have also captured much more statistics and allowed many different ways of viewing the data within the tool.
• Exporting the data. There are multiple ways to send and export data.
• Fixing the bug. I have also considered the process of visiting and fixing the data, and preventing some types of errors from appearing in future scans. This process is much like how Outlook allows one to manage inbox message.

I suspect that this product will be much more pleasing to the eyes and richer in functionality than people will have been expecting.

Loops, Part 2

This is the second in a multi-part series on loop handling, which will be followed by treatments on methods, state, and other interesting areas of static analysis.

I have tried to be as general as possible in my code analysis, while still remaining efficient, such as in how I deal with state, function calls, loops and recursion.

One illustration of this is how I represent newly allocated objects or the return values of unknown functions from inside loops. There were several methods that I considered, each with different tradeoffs, but the method I ultimately decided upon because it was more composable (thereby making analysis easier) and more understandable for the user.

In the following example, I allocate elements for an array.

When allocating a new object, a new id is required to uniquely identify the object, since the "new object()" expression is not sufficient to distinguish two different allocations. Rather than incrementing a counter which could be used for generating an id number, I preferred tying the id to the object's location in the source code; this way, the id could remain a constant number without the likely risk of turning into a complex expression as would happen with the alternate method.

However, this method is not sufficient inside loops or in repeated function calls, so we need a loop identification operator to identify the iteration within the loop in which the object was allocated.

The locals window shows how the operators for object identification and loop interation appear. Object identification uses the "#" symbol and loop iteration reuses "{}". I drop the id for the array assigned to the "array" variable, since every instance of that array will be referred to by the "array" variable name; the id in that case becomes pure noise.

I have shown some examples of the values of various array elements, including one (contained in the local "w") indexed by a variable. The loop iteration is very easy to understand and just as well to analyze.

I should note the w is not fully simplified as it is possible to remove the lambda expression with a quotient and remainder operator; this will probably be fixed before I release.

In this simpler example, I show that objects allocated at different instances of the loop are not equal. I also expanded the array variable to expose the values of each of the elements of the array.

* The value produced here by the array.Length variable is a bug, which has not been fixed yet, and should actually report the number 3.

NStatic Plans

Update

In my last post, I just mentioned some thoughts about where I would be going with the post-V1. I not making major development changes at this point, so as not to delay the product any longer. Even before adding WPF and developing with Orcas, though, there are quite a few items such as VB.NET and partial or complete C# 3.0 support as well as other postponed items such as specifications that are relatively easy to add.

This week I am going through the user interface and getting the final appearance down and fixing all the little UI and keyboard issues. I moved up the Scan window from a docked pane to a ribbon tab per Scott Hanselman’s suggestion. It’s almost July… I don’t want to still be worrying about UI after this month; I am growing tired and want the program out.

I won’t be posting much this week. I’ll post more NStatic examples next week, revealing a few more aspects of the tool for the first time. These posts will make it easier for me to pull together documentation before I ship.

Market Plans

After I ship, there are some proposals I will be entertaining from a few companies. So, I may be selling NStatic independently for a few months before any deal is finalized, after which the price will likely go up dramatically; bargain hunters might want to buy early. For now, I am continuing on my original plans.

Part of my original viral strategy was to get people used to NStatic by making a minimal version of the software, which could also act as a Ribbon-based notepad clone with enhanced editing capabilities—maybe pull people into purchasing the full version. This goes with other forms of traditional marketing—PR, advertising, etc. I am not currently sure now how I will have people evaluate my software.

I am hoping that maybe, just maybe, that, with a unique sophisticated static analysis product that’s a must buy, I might be able to capture some percentage of the .NET developer marketplace. Other categories such as unit-testing, component libraries, source control, text editors, obfuscation, refactoring tools, bug-tracking are heavily fragmented with many competitors or face freely available alternatives. I am effectively all alone with an advanced technology and no overhead, too, so I can underprice any large competitor. This ties in with the central message I got from my business school’s strategy course, which is to “avoid competition.” (For example, Walmart eventually overtook Kmart because most Walmart stores were local monopolies based in rural areas.)

How big is this market, though? I used to have data on market sizes of different software application categories, but since I left business school, I lost access to all sorts of privileged market data. I have to rely on serendipitous information, such as slips by Microsoft executives about there being over 1 million Visual Studio 2005 shipments and 15 million VS Express downloads.

Market information is hard to extract from the web, but I did find a bevy of information from O’Reilly’s Radar weblog on the State of the Computer Book Market (Q1 07). The numbers come from a database containing information about Bookscan’s weekly top 10,000 titles sold. Approximately, 200K books on C# and an additional 120K books on .NET are sold each year. Visual Basic books sell at half the rate of C# books, so I could get a 50% boost in sales by including VB support.

The data also suggests that porting to Java and C++ would each effectively double my C# sales, which are not currently in my plans. I don’t want to damage the business model of companies with top-notch researchers who dedicated their lives to source code analysis. I don’t have a tight attachment to source code analysis; I am just applying my symbolic AI techniques to different application areas.

Loops, Part 1

I was hoping to post at a rate of once a day highlighting some area of NStatic, but I have found myself busy eliminating bugs. This is my first post on loops, but I will likely be expanding on it on the future.

One feature that is possibly unique to NStatic is the exact treatment of loops. Other products tend to examine loops a fixed number of iterations (usually just once) or simply punt on the issue.

Variables that are changed within loops are converted into expressions containing functions or closed forms of specially recognized functions. In this example, I will use the Fibonacci function. The Fibonacci function returns the nth element of the sequence

1,1,3,5,8,13,21,34,55,...

It's alternatively expressed as a recurrence relation:

Fib(0) = 1
Fib(1) = 1
Fib(n) = Fib(n-1) + Fib(n-2)

Below are two alternate implementations of the Fibonacci function, one which is recursive and another which is implemented imperatively via for loops.

I have also included below a goto version of the for loop to show that loops are handled in a general way and that I offer no special treatment for the for loop operator.

Below is the actual result at the breakpoint in the FibGoto function.

The values of both prev and sum are expressible in closed forms. The closed form of the Fibonacci function is well-known and is expressed as the sums of the powers of the golden ratio (and its difference from one), all divided by the square root of five. However, I did not hardcode the formula, since the Fibonacci function falls into a general class of second-order homogenous recurrence formulas.

The function FibTest computes the results of the earlier three implementations of the Fibonacci function. Note that I pass in a double to the recursive function, so it doesn't produce a closed form. (The closed form can probably be generated by taking the ceiling of the floating-point value before applying the function.)

The output for FibTest is shown below.

Equation Solving

One of the side benefits of the NStatic Tool is the ability to solve various types of equations or systems of equations. One set of problems is the solving of systems of equations in linear algebra.

In the example above, we have three equations with three unknowns. Since all three equations are linearly independent, we are guaranteed a single solution as revealed below by NStatic.

I kept the parameter types as doubles, since even though all the coefficients are integers, we could easily get a solution set that incorporates numbers from the rational domain.

Just by changing the integer constant in the right hand side of the last equation from 10 to 11, all of the values would have to be rationals, and last assert would no longer be satisfiable if any of the parameter variables were declared an int.

The value column depicts all of the solutions values in rational form (with a numerator and denominator), even though they were declared as doubles. The use of rational numbers ensures against rounding errors, which could easily introduce hard-to-find bugs into the system.

Another set of problems are polynomial equations. NStatic has the ability to solve polynomial equalities and inequalities. Nonlinear equations arise quite commonly with recursion and looping control structures.

Here I have a loop that computes the sum of an arithmetic sequence and then performs a test on the sum.

In this case, we are able to place a bound on the value of n to ensure that the sum is over 20. The variable sum is a quadratic polynomial of a complex term, so we can find the roots of the equation to come out with a disjunction of all the possible ranges of n.

 

Execution Paths

There were a few items that I didn't show in previous posts on my attempts at visually illustrating execution traces leading to an error or breakpoint.

One is the superimposing of arrows of all possible paths together. For all errors or breakpoints of the same type in the same location with the same call stack, all possible paths leading to the error are shown simultaneously. This has interesting consequences inside various control structures such as finally clauses, loops.

For one thing, this does means NStatic's reported error count will actually be an underestimate of the number of errors it found, as each reported error count represents multiple bugs. On the other hand, it cuts down on false positive rates in which not every possible path will likely be explored in actual use.

There are some reasons for this. For example, there may be an exponential number of paths leading to the error, so it would not be possible for me enumerate all of them. I do plan on providing a later option in a minor update where additional assumptions may applied after the fact to selectively choose which arrows are most important.

In the bug above, there is a warning given for the cases where we may encounter an error. Inactive code in the function is blanked out.

The execution path is general. From within a function, all types of control structures are supported and accurately depicted from arbitrary gotos, throws, loops, finally clauses. Probably, the main limitations are due to asynchronous exception handling (thread aborts, stack overflows, out of memory), which I am still thinking about. The execution path is shown for all functions in the current call stack, but it would not be difficult in the future to add support for examining the traces of previously completed functions that have vanished from the call chain.

The implementation is simple but completely general--a real functional pearl. The execution path is internally represented as an expression with a sequence operator, which is only simplified with current set of assumptions at the time the user views the error. The expression becomes arbitrarily complex with lambda functions and conditionals.

Coming Along

NStatic is not yet in beta. I have a couple of people on NStatic, and am still fixing a number of bugs.

I also have events going on in my life. (surprise) My parents and siblings flew in the first week of May to visit me, which I targeted mid-to-late date for closure, since these events are disruptive to my flow. I have also been unexpectedly invited to a Microsoft compiler lab event next week to attend, which will most likely be focused on recent announcements such as Silverlight, DLR and the Orcas beta.

It'll be beta when it's ready; stuff takes time to cook. There are no more major changes or additions; the existing feature set is good enough.

Quantification

Spec# and JML both support quantification operators like forall and exist as seen in lines 9 and 10 of this Spec# code sample:

   1:  class ArrayList { 

   2:  void Insert(int index , object value)

   3:      requires 0 <= index && index <= Count

   4:          otherwise ArgumentOutOfRangeException;

   5:      requires !IsReadOnly && !IsFixedSize

   6:          otherwise NotSupportedException;

   7:      ensures Count == old(Count) + 1;

   8:      ensures value == this[index ];

   9:      ensures Forall{int i in 0 : index ; old(this[i]) == this[i]};

  10:      ensures Forall{int i in index : old(Count); old(this[i]) == this[i + 1]};

I don’t actually directly support quantifiers in the reasoning system used by NStatic. However, because the system completely support functions, quantifiers are actually redundant; I can reduce quantifiers to equivalent unquantified functional expressions.

The most common use of quantifiers seems to be iterating over all elements of an array. In such cases, quantifier keywords can be imitated by C# language constructs.

For the expression Forall{int i in index : old(Count); old(this[i]) == this[i + 1]} from the above code.

     for (int i = index; i < oldCount; i++)
           Debug.Assert(oldArray[i] == newArray[i+1]);

Alternatively and equivalently, the same test could be rewritten as a function called inside of an Assert statement.

    bool TestArray(int[] oldArray, int[] newArray, int index, int oldCount)
    {
        for (int i = index; i < oldCount; i++)
            if (oldArray[i] != newArray[i+1])
                return false;
        return true;
    }

    Debug.Assert(TestArray(oldArray, newArray, index, oldCount);

In the first case, the Assert statement was inside the loop and, in the second case, it was left outside. In either case, they both perform the same operation and are, therefore, normalized to same internal representation.

This illustrates the basic operation of NStatic. Within the limits of the simplifier inside NStatic, straightforward, equivalent fragments of code are normalized to the same representation, regardless of constructs used.

We could define quantification operators more generally as higher-order functions:

[Conditional("CODEANALYSIS")]
bool ForAll(int start, int end, Func<int, bool> predicate)
{
     for (int i = start; i <=end; i++)
           if (!predicate(i))
                 return false;
     return true;
}

[Conditional("CODEANALYSIS")]
bool ThereExists(int start, int end, Func<int, bool> predicate)
{
     for (int i = start; i <=end; i++)
           if (predicate(i))
                 return true;
     return false;
}

Debug.Assert(ForAll(i, index, oldCount-1, 
     delegate(int i) { return oldArray[i] == newArray[i+1]; });

Other types of quantifiers could also be created this way such an existential uniqueness operator. The initial release of NStatic though will probably not have enough simplifications to enable these other quantifiers, due more to lack of time rather than any implementation difficulties.

I inserted the "Conditional" attribute is there simply to avoid compilation into code. Otherwise, the C# compiler would happily compile the code and, if the difference between start and end happened to be a large value like int.MaxValue, the runtime execution of this code could hang for a long time.

NStatic doesn't execute recursive functions and loops, unless such expressions are determined to terminate in a short amount of time and space. Instead, NStatic evaluates loops and recursive functions symbolically by recognizing patterns in the loop and simplifying them, allowing its analysis of the same expression to proceed quickly.  The simplified representation of the loop is then used as its value.

For quantifying over non-indexable sets, we could have functions over collections or functions that walk through composite data structures. To quantify over all the objects in the heap, though, it would seem we may need a special quantifier keyword or class invariants, which I won't be adding until support for specifications in a future version.

Bug Tracking

I have just set up a Fogbugz bug-tracking site for the upcoming beta of NStatic at http://nstatic.fogbugz.com. I have over a hundred people on my beta list, and this is where the bug-reporting action is going to be.

The site uses FogBugz On Demand (beta) and includes a page for case entry and also discussion groups, of which I have already set up two. Feel free to post any new topics in the discussion groups.

I have only been using FogBugz for a day and am really enjoying. It’s very similar to the bug-tracking system that I used at Microsoft. My ex-wife, an actual software tester, has agreed to post and regress bugs for me.

Estimation

SecretGeek recently has two articles on software estimation:

• Are We There Yet? Using Circles to Measure Progress
• Why Accurate Estimations are Just Not Possible

I didn’t make my April 15th, but I think I am close to a beta release. I went through the first week sick, possibly through chemical poisoning while cleaning, and just lost my flow.

I don’t think that are any real hard issues left. In the past couple months, I made some major changes to remove performance bottlenecks and eliminate limitations. I refactored my core analysis routines to enable unlimited function call depth and to better support symbolic IL interpretation. Every data structure had to support recursion. I also rewrote my theorem prover for logical expressions. It’s completely deterministic now and dramatically faster. I basically discovered an breathingly new algorithm, that is purely functional and fits in just over 1000 lines of code.

For over a year, each month that I have been developing this software product, the performance has improved tenfold, which isn’t hard in a category of software where exponential running times are common place. The performance improvements manifested itself in shorter scanning times and fuller, deeper analyses. This includes going from limited function call depth to almost no restrictions, from hours long analysis to times approaching compilation. I also went from a several dialog options for tuning analysis to none, because the software simply became smart enough that the options were no longer needed.

I still have a number of surprises in store that I haven’t shown yet. There’s still some aesthetics and UI issues to work out during the beta. I plan on getting my some local testers playing with the tool late next week and sending bug reports via Fogbugz, after which I hope to be sending a future weekly builds out to an expanding pool of testers.

Spec# is Out

Spec# for Visual Studio 2005 is out now… Perhaps, we will see this along with Pex in the version of VS following Orcas. Here’s the description of Spec# in the Microsoft Research site:

Spec# is an experimental language that extends C# with several design-by-contract features. The new features of Spec# include a non-null type system, method pre- and post-conditions, loop invariants, and object invariants. The Spec# Programming System provides design-time checking, run-time checking, and a static verifier. This version of Spec# runs on .NET Framework version 2.

Static Analysis Tools at the Summit

The MVP Summit saw three different demos of various static analysis tools demoed to MVPs. I know all of the developers of the tools and even hinted at times at whether we should provide some links or integration, since our tools have somewhat mutually exclusive functionality.

Serge Baranovsky demonstrated his beta analysis tool, CodeIt.Right, which is similar to FXCop, but offers refactoring capabilities. Serge actually lives close to me and attend my NStatic presentation in February.

Patrick Smacchia demonstrated NDepends 2.0. Raymond Lewallen [MVP] reported that NDepend made a huge splash in Redmond.

I couldn't be happier for my friend Patrick Smacchia - the creator of NDepend.  Anybody who knows me knows that I am NDepend's biggest fan, other than Patrick himself, and really, really want to see the product hit mainstream use and make Patrick rich beyond his wildest dreams!

There wasn't a day that went by that I wasn't able to talk to Patrick, but that was quite difficult.  You see, everytime I ran into Patrick, he was being mobbed by groups of developers that were amazed at what NDepend is able to do, and what you are able to do with it.  There is no telling how many times he demo'd his product (he even had the opportunity to demo his product to a Microsoft developer group in private), but his enthusiam for the product is matched by nobody, and its great to see how his excitement during demos is passed into those around him, getting them just as excited about the product.

Its amazing to see how many people still do not understand code metrics and how easily available the information is.  And then to add on a query language - that just blows people's minds.

This follows from Raymond’s post last month comparing NDepend with new code metrics in Orcas March CTP.

… However, VS code metrics have a long, long ways to go before its going to be something that I use for serious analysis.  That's where NDepend comes in.  NDepend supplies over 60 quality and useful code metrics, and also has its own query language that Patrick calls CQL.  Its easy to use and is part of my formal build process.  Its going to be very hard for anything to dethrone NDepend as the king of code metrics.

I demonstrated NStatic to about a dozen people including Patrick Smacchia, Raymond Lewallen, Scott Hanselman. One idea mentioned to me separately by both Patrick and Scott was the incorporation of code metrics given the amount of semantic knowledge I extract. I could even invent my own metrics. [UPDATE: Raymond also mentioned my product in a post “Another big splash in Redmond – NStatic.”]

Parameterized Unit Tests

Andrew Stopford wrote about a Microsoft Research technology called parameterized testing being developed on a project called Pex (Program EXploration). Pex is described as an…

…intelligent assistant to the programmer. By automatically generating unit tests, it allows [one] to find bug early. In addition, it suggests to the programmer hot to fix the bugs.

In addition to specifications, I have been thinking since last spring about how I could better integrate my software with unit-testing. While I am not planning on building a dedicated system like Pex, one common trait that my system may have with Pex is the ability to symbolically analyze a function with unspecified parameters. 

Some of the changes that I had been considering included:

• Recognizing calls to the various unit-testing frameworks such as Assert.IsTrue.
• Accepting test methods containing parameters.
• Presenting an NUnit style tree-view interface.

In addition, NStatic would not actually cause any external side-effects to the environment, which may or may not be a benefit. Also, there may also be some cross-pollenation and integration with the specifications work post-V1.

It’s not entirely clear to me at the moment what additional value the last two bullet points have over just performing a regular scan over the codebase (and/or using specifications): Automatic calls to Setup and Teardown? More structured tests? Exploring specific scenarios?

These are just some of my thoughts for the long-term future of my product. None of these features are coming out in the first version.

Anonymous Recursion

I was planning on writing about anonymous recursion relating to work in NStatic, but Wes Dyer beat me to the punch with his post Anonymous Recursion in C#. In addition to my name, Wes Dyer shares my desire to push a more functional style of programming in C# (and he's also a member of the C# team, so we may win).

 

Loops and recursive functions in NStatic are converted to recursive lambda expressions, and then through various techniques like unrolling, recurrence solving, inductive proofs, are simplified to a closed form. The expressions above are intentionally unsimplified for illustrative purposes. 

Each of the lambda expressions displayed above are recursive. Nonrecursive lambda expressions are applied over their arguments, so they aren't normally seen unless standalone without any arguments.

I am not currently sure how I will eventually display lambda expressions in C#; the current display is attractive to my eyes, personally, but may turn off users unfamiliar with lambda calculus. I probably will ultimately go with a more C#-like syntax. My previous attempt was quite unreadable or quite verbose because the lambda operator => looks like the inequality operator and the use of parenthesis was quite excessive. Another possibility is to use C# 2.0 syntax with delegate and return keywords.

For those with sharp eyes, I introduced a fix operator to concisely display recursive lambda expressions. The fix function takes as its argument any lambda expression that includes a first parameter, representing the name of the function itself. That parameter can be used inside the lambda expression to recursively call itself.

In a language that does not explicitly have recursion operators, lambda expressions can be used to introduce recursion. It's not very pretty, but one such operator to do this is called the Y fixed-point combinator.

    public delegate Func<X,T> YFunc<X,T>(YFunc<X,T> f);
    public static Func<X, T> YCombinator<X, T>(Func<Func<X,T>, Func<X,T>> f)
    {
        YFunc<X,T> lambda = delegate(YFunc<X,T> y)
        {
            // return f(y(y)); -- only works with call by name
            return f(delegate(X x) { return y(y)(x); });
        };
        return lambda(lambda);
    }

The combinator does not allowed to use recursion, only function application, in its definition, since it's purpose is to introduce a form of recursion in the first place.

The Y combinator is possible in a typed language like C# because C# allows us to recursively define types--that is, YFunc was defined in terms of itself. A slight modification, an additional lambda expression, was also needed to allow f(y(y)) to be called by name.

A more efficient function for anonymous recursion takes advantage of assignment in the C# to avoid the creation of more than one closure is the following function.

    public static Func<X, T> Fix<X, T>(Func<Func<X,T>, Func<X,T>> func)
    {
        Func<X,T> fixfunc = null;
        fixfunc = func(delegate(X x) { return fixfunc(x); });
        return fixfunc;
    }

An example of its use in C# is the following:

    Func<int,int> func = Fix<int,int>(
        delegate(Func<int,int> f)
        {
            return delegate(int n)
            {
                return n<=1 ? 1 : n + f(n-1);
            };
        });
    
    Console.WriteLine(func(6));

NStatic Presentation, II

This is a continuation of my previous post NStatic Presentation.

This half of the presentation was more about technical details. Many in the audience didn't really seem to understand what I was trying to say.

Slide# 11 -- Smarter Analysis

I stated in my presentation that my goal in this product is the illusion of true understanding. What do I mean by true understanding? Well, I think it's somewhat like the Turing test, which claims that a machine could be said to think, if it is indistinguishable in behavior from a human being.

Can I achieve some semblance of a human-like intelligence in my tool, with performance that is indistinguishable from a code reviewer with no prior experience with the code base? I am still far away from that point by my reckoning, but there are three important ingredients that get me closer to the dream: Symbolic manipulation, interprocedural analysis, and the application of general abstract principles rather than specific rules.

Slide #12 - 13 - Symbolic Manipulation

• Everything is represented by expressions, manipulated algebraically
• Expressions are reduced to canonical form
  • Fast, but requires many transformation rules
  • May contain lambda and conditional operators
  • Higher-order functions are naturally supported
• Advantages of thinking symbolically
  • Analyze code fragments in isolation
  • Effectively deal with unknowns and ambiguities

The data structure that I used store and represent values is an expression in a symbol functional language, based on lambda calculus. Since the language is Turing-equivalent, we can represent and evaluate the value of any variable in the program. What's important is that operations in this language can work directly with symbols rather than numbers. (Numbers by the way are just accidents. While numbers in C-based language seems to be omnipresent, programs are regularly written in sizable functional languages like Lisp and Haskell without any use of numbers.)

Slide #14 - Symbolic Manipulation: Arithmetic

Through the magic of functional pattern matching, we evaluate expressions by replacing patterns with the expression with simpler forms that known to be equivalent. When we evaluate expressions in this way, the result is often a simplified version in a canonical normal form. The benefit of reducing expressions to normal forms is that we can quickly compare them two expressions for equality. 

The examples below illustrate some basic simplifications of arithmetic and comparison operations.

Slide #15 - 17 - Symbolic Manipulation: Conditionals

Our symbolic manipulation also extends to conditionals as depicted in the following example.

Traditionally, instead of constructing a functional if expression, a static analyzer might either use ternary values (true, false, don't-know), in which case data would be marked with "don't-know," or the analyzer might insert into a knowledge base a disjunctive clause such as p < 1 && data == "hello" || p >= 1 && data == null.

Here we see the value of data in an extended version of the previous code. Because we know the value of p, we actually can simplify the value of data to "hi."

The conditional operator arises naturally in other contexts such as when a field accessor is being modified.

Slide #18 - Symbolic Manipulation: Loops

• Denotational Semantics

Each procedure is converted to side-effect- free functions

• Completely general, precise translation
• No more dichotomy: control flow becomes data
  • Imperative constructs converted to equivalent functional form in lambda calculus
  • Control statements are modeled using recursive lambda expressions instead of a control flow graph

We use denotational semantics to represent our code. A functional representation can be analyzed and simplified much more easily.

Changed loop variables are assigned the result of an applied recursive lambda expression or a closed form thereof.

This gives us the ability to relate the results of loops with each other and with other functions. In this example, if fact is a recursive method that computes the factorial function, then f==fact(n) would be true, since they have the same canonical form.

Slide #19 - 22 - General Principles

I spoke about General Principles versus Specific Rules in a prior blog post on "Intelligence versus Intellisense." I wrote of a basic philosophical goal of mine, which is to replicate the actual human reasoning process as faithfully as possible, often choosing less efficient methods for better fidelity.

One of the first types of analysis is Exception Analysis:

• Exception Analysis
  • System exceptions
  • User-defined exceptions, unequivocally fired
  • Failed asserts
  • Framework parameter validation via IL interpretation

The tricky part is determining whether an exception is fired.

Another type of analysis relies on notions of redundancy and effectiveness.

• Notions of Redundancy and Effectiveness
  • Compares expressions and state of the world before and after evaluation
• Examples
  • Complex expressions (including function calls) that evaluate to constants
  • Assignment to a variables is same as current value
  • Redundant parameter - parameter is a function of other parameters/globals
  • Infinite loops, no side effects

Again the difference here from other products is how I actually compare expressions and the state of the world before and after evaluation. Nothing is based on low-level analysis of syntax but rather a higher-level semantic analysis.

Slide #23 - Interprocedural Analysis

An important part of understanding code is knowing the relationships between each of the methods. Analyzing each method in isolation doesn't lead to intelligent analysis, if all the callee functions are not examined.

Below is a call stack window showing a stack trace in Rotor, depicted an interprocedural call.

I also brought up the point of the "Ghetto," which is how existing tools focus only on primitive types and low-level system exceptions like null references.

I do want to move beyond that point and get out of the ghetto, finding errors on complex, user-defined types and functions, not just primitive types. I also want to effect manipulate higher-order functions.

Slide #24 - IL Interpretation

Closely connected with interprocedural analysis is IL interpretation. We could analyze our codebase, but still miss a big part of code that is executed. The framework and third-party libraries are just as important for intelligent static analysis.

Since I discovered a way to perform interprocedural analysis very quickly, it made sense for me to pursue IL interpretation of system frameworks, rather than hardcode parameter validation.