Simpler specifications for resource-manipulating programs