Previous article

Next article

The Correctness of the Definite Assignment Analysis in C#

Nicu G. Fruja, Computer Science Department, ETH Zürich, Switzerland

space PDF Icon
PDF Version


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


Cite this article as follows: Nicu G. Fruja: “The Correctness of the Definite Assignment Analysis in C#”, in Journal of Object Technology, vol. 3, no. 9, October 2004, Special issue: .NET Technologies 2004 workshop, pp. 29-52. http://www.jot.fm/issues/issue_2004_10/article2

Previous article

Next article