.NET TECHNOLOGIES 2004 WORKSHOP, PILSEN

Previous article Next article

---

The Correctness of the Definite Assignment Analysis in C# Nicu G. Fruja, Computer Science Department, ETH Zürich, Switzerland

PDF Version

Abstract

The compilation of C# requires a flow analysis to ensure that every local variable is definitely assigned when any access to its value occurs. A variable is definitely assigned at a use of its value if every execution path leading to that use contains an assignment to the variable. Since local variables are uninitialized by default, this prevents access to uninitialized memory which is a crucial ingredient for the type safety of C#. We formalize the rules of the definite assignment analysis of C# with data flow equations and we prove the correctness of the analysis, i.e. if the analysis will infer a local variable as definitely assigned at a certain program point, then the variable will actually be initialized at that point during every execution of the program. We actually prove more than correctness: we show that the solution of the analysis is a perfect solution (and not only a safe approximation).

Note: Due to the typographical sophistication of this column, no HTML version is available. Please use the PDF version.

About the author

Nicu G. Fruja is a PhD student and research assistant at the Computer Science Department at the ETH Zürich, Switzerland. His research interests are in the areas of formal methods, specification, verification and validation of systems, abstract state machines, semantics of programming languages, bytecode verification. He can be reached at fruja@inf.ethz.ch. See also http://www.inf.ethz.ch/personal/fruja/.