Fixed getOffset() JML and added JML specs to other funcs