NStatic

57 posts

NStatic

I started working on NStatic a little under a decade ago. It went through several iterations of development with major design changes that broke a lot of functionality in order to achieve the product I dreamed of. For instance, one goal was to be able to prove the correctness of an implementation of red-black trees. I have seen papers in computer verification in which every loops had to be proved with some Hoare logic annotations. Assertions contain forall and exists quantifiers when using a function call was far simpler to use and read; function calls are actually more efficient to...

Plans for Year 2015

My company is SoftPerson, which specializes in “semantic computing” in everyday general-purpose applications. The past decade or so was one of a lot of reading, research and experimentation with entirely new technologies and user experiences, but no product. I can’t really continue for more than another year without revenues, so I came up with some remedies. These are my plans for the current year. Releasing a NConvert semantic code conversion tool early this year Kickstarter for NStatic, a static analysis tool, next month (In a future year, I would do the same for my natural language wordprocessor product). In both...

Specification Languages

Specification Languages I have not had any instruction in formal methods, so I really didn’t encounter specification languages in my coursework, but I have read papers on proving programs including some classic papers by Hoare and Djikstra, and was familiar with Eiffel contracts. At Harvard, I audited the first couple lectures of graduate level computer science course in Software Engineering, but never encountered modeling and specification in the initial lectures. (By the way, this instructor, a guest lecturer from industry, following custom, recounted his prior interactions with Bill Gates. He did indeed have Bill as a student, and proudly proclaimed in his...

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...

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...

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...

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...

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...

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...

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......

© 2015 - Wesner P. Moise, LLC. All rights reserved.

free web stats