A framework for prototyping and reasoning about grid systems