Verifying OCL pre/post condition using Cyclone. - YueLou Ding; Hao Wu 017 (STAF Workshops, 2025)