A JML-Based strategy for incorporating formal specifications into the software development process

This thesis presents a JML-based strategy that incorporates formal specifications into the software development process of object-oriented programs. The strategy evolves functional requirements into a “semi-formal” requirements form, and then expressing them as JML formal specifications. The strategy is implemented as a formal-specification pseudo-phase that runs in parallel with the other phase of software development. What makes our strategy different from other software development strategies used in literature is the particular use of JML specifications we make all along the way from requirements to validation-and-verification.

On invariant Rings of Sylow subgroups of finite classical groups

In this thesis we study the invariant rings for the Sylow p-subgroups of the nite classical groups. We have successfully constructed presentations for the invariant rings for the Sylow p-subgroups of the unitary groups GU(3; Fq2) and GU(4; Fq2 ), the symplectic group Sp(4; Fq) and the orthogonal group O+(4; Fq) with q odd. In all cases, we obtained a minimal generating set which is also a SAGBI basis. Moreover, we computed the relations among the generators and showed that the invariant ring for these groups are a complete intersection. This shows that, even though the invariant rings of the Sylow p-subgroups of the general linear group are polynomial, the same is not true for Sylow p-subgroups of general classical groups. We also constructed the generators for the invariant elds for the Sylow p-subgroups of GU(n; Fq2 ), Sp(2n; Fq), O+(2n; Fq), O-(2n + 2; Fq) and O(2n + 1; Fq), for every n and q. This is an important step in order to obtain the generators and relations for the invariant rings of all these groups.