In previously described uniqueness extensions to imperative languages, a unique variable can be accessed only with a destructive read, which nullifies it after the value is obtained. This approach suffers from several disadvantages: the use of destructive reads increases the complexity of the program which must continually restore nullified values; adding destructive reads changes the semantics of the programming language; and many of the nullifications are actually unnecessary.
We demonstrate instead that uniqueness can be preserved through the use of existing language features. We give a modular analysis that checks (nonexecutable) uniqueness annotations superimposed on an imperative programming language without destructive reads.