Optimizing Generated Aspect-Oriented Assertion Checking Code for JML Using Programming Laws: An Empirical Study - Henrique Rebêlo; Ricardo Lima; Gary T. Leavens; Márcio Cornélio; Re Mota; César Oliveira; The Pennsylvania State University CiteSeerX Archives (http://www.eecs.ucf.edu/ leavens/tech-reports/UCF/CS-TR-10-01/TR.pdf, 2010)