"Sealed Class and Interface" feature of "OpenJDK-17" on JPF/java-17

[eklaDFF]

@cyrille-artho
@pparizek

Sealed Class Tests

package java17;

import gov.nasa.jpf.util.test.TestJPF;
import org.junit.Test;

public class SealedClassTest extends TestJPF {

    sealed class Shape permits Circle, Square, Rectangle {

    }

    final class Circle extends Shape {

    }

    final class Square extends Shape {

    }

    non-sealed class Rectangle extends Shape {

    }

    class CustomRectangle extends Rectangle {

    }

    @Test
    public void testCircleInstance() {
        if (verifyNoPropertyViolation()){
            Shape shape = new Circle();
            assertTrue("", shape instanceof Circle);
        }
    }

    @Test
    public void testSquareInstance() {
        if (verifyNoPropertyViolation()){
            Shape shape = new Square();
            assertTrue("", shape instanceof Square);
        }
    }

    @Test
    public void testRectangleInstance() {
        if (verifyNoPropertyViolation()){
            Shape shape = new Rectangle();
            assertTrue("", shape instanceof Rectangle);
        }
    }

    @Test
    public void testCustomRectangleInstance() {
        if (verifyNoPropertyViolation()){
            Shape shape = new CustomRectangle();
            assertTrue("", shape instanceof CustomRectangle);
            assertTrue("", shape instanceof Rectangle);
        }
    }
}

All the above Tests passes.

---

Sealed Interface Tests

package java17;

import gov.nasa.jpf.util.test.TestJPF;
import org.junit.Test;

public class SealedInterfaceTest extends TestJPF {

    sealed interface Shape permits Circle, Square, Rectangle {

        double area();
    }

    final class Circle implements Shape {

        private double radius;

        public Circle(double radius){
            this.radius = radius;
        }

        @Override
        public double area(){
            return (Math.PI * radius * radius);
        }

    }

    final class Square implements Shape {

        private double length;

        public Square(double length){
            this.length = length;
        }

        @Override
        public double area() {
            return (length * length);
        }
    }

    public non-sealed class Rectangle implements Shape {
        private double length;
        private double width;

        public Rectangle(double length, double width) {
            this.length = length;
            this.width = width;
        }

        @Override
        public double area() {
            return (length * width);
        }
    }

    public class CustomRectangle extends Rectangle {
        public CustomRectangle(double length, double width) {
            super(length, width);
        }
    }

    @Test
    public void testCircle() {
        if (verifyNoPropertyViolation()){
            Shape shape = new Circle(5);

            // Test Circle Instance
            assertTrue("",shape instanceof Circle);

            // Test Circle "area"
            assertEquals(Math.PI * 25, shape.area());
        }
    }

    @Test
    public void testSquare() {
        if (verifyNoPropertyViolation()){
            Shape shape = new Square(4);

            // Test Square Instance
            assertTrue("",shape instanceof Square);

            // Test Square "area"
            assertEquals(16, shape.area());
        }
    }

    @Test
    public void testRectangle() {
        if (verifyNoPropertyViolation()) {
            Shape shape = new Rectangle(3, 7);

            // Test Rectangle Instance
            assertTrue("", shape instanceof Rectangle);

            // Test Rectangle "area"
            assertEquals(21, shape.area());
        }
    }

    @Test
    public void testCustomRectangle() {
        if (verifyNoPropertyViolation()){
            Shape shape = new CustomRectangle(4, 5);
            Rectangle rectangle = new CustomRectangle(3,4);

            // Test CustomRectangle Instance
            assertTrue("",shape instanceof CustomRectangle);
            assertTrue("",rectangle instanceof CustomRectangle);

            // Test CustomRectangle "area"
            assertEquals(20, shape.area());
        }
    }
}

All the above Tests passes.

[cyrille-artho]

Looks good; provide some comments that give a rationale behind the chosen class hierarchy (what aspects of sealed/non-sealed class behavior is tested by which test).

[eklaDFF]

Sealed Class Tests

package java17;

import gov.nasa.jpf.util.test.TestJPF;
import org.junit.Test;

public class SealedClassTest extends TestJPF {

    // Shape is a "sealed" class, and it allows only "Circle", "Square" and "Rectangle" to extend.
    sealed class Shape permits Circle, Square, Rectangle {

    }


    // Here "Circle" class is allowed to extend "Shape". Sealed class "Shape" allows "Circle" to extends in "permits" clause.
    // But "Circle" is "final class" so it cannot be extended by anyone more.
    final class Circle extends Shape {

    }


    // Here "Square" class is allowed to extend "Shape". Sealed class "Shape" allows "Square" to extends in "permits" clause.
    // But "Square" is "final class" so it cannot be extended by anyone more.
    final class Square extends Shape {

    }


    // Here "Rectangle" class is allowed to extend "Shape". Sealed class "Shape" allows "Rectangle" to extends in "permits" clause.
    // But "Rectangle" is "non-sealed class" so it can be extended by anyone more.
    non-sealed class Rectangle extends Shape {

    }


    // Here "CustomRectangle" class is allowed to extend "non-sealed class Rectangle".
    class CustomRectangle extends Rectangle {

    }

    @Test
    public void testCircleInstance() {
        if (verifyNoPropertyViolation()){
            Shape shape = new Circle();
            assertTrue("", shape instanceof Circle);
        }
    }

    @Test
    public void testSquareInstance() {
        if (verifyNoPropertyViolation()){
            Shape shape = new Square();
            assertTrue("", shape instanceof Square);
        }
    }

    @Test
    public void testRectangleInstance() {
        if (verifyNoPropertyViolation()){
            Shape shape = new Rectangle();
            assertTrue("", shape instanceof Rectangle);
        }
    }

    @Test
    public void testCustomRectangleInstance() {
        if (verifyNoPropertyViolation()){
            Shape shape = new CustomRectangle();
            assertTrue("", shape instanceof CustomRectangle);
            assertTrue("", shape instanceof Rectangle);
        }
    }
}

---

Sealed Interface Tests

package java17;

import gov.nasa.jpf.util.test.TestJPF;
import org.junit.Test;

public class SealedInterfaceTest extends TestJPF {

    // "Shape" is a "sealed" interface, and it allows only "Circle", "Square" and "Rectangle" to implement.
    sealed interface Shape permits Circle, Square, Rectangle {
        double area();
    }


    // Here "Circle" class is allowed to implement "Shape". Sealed interface "Shape" allows "Circle" to implement in "permits" clause.
    // But "Circle" is "final class" so it cannot be extended by anyone more.
    final class Circle implements Shape {
        private double radius;

        public Circle(double radius){
            this.radius = radius;
        }

        @Override
        public double area(){
            return (Math.PI * radius * radius);
        }

    }


    // Here "Square" class is allowed to implement "Shape". Sealed interface "Shape" allows "Square" to implement in "permits" clause.
    // But "Square" is "final class" so it cannot be extended by anyone more.
    final class Square implements Shape {
        private double length;

        public Square(double length){
            this.length = length;
        }

        @Override
        public double area() {
            return (length * length);
        }
    }


    // Here "Rectangle" class is allowed to implement "Shape". Sealed interface "Shape" allows "Rectangle" to implement in "permits" clause.
    // But "Rectangle" is "non-sealed class" so it can be extended by anyone more.
    public non-sealed class Rectangle implements Shape {
        private double length;
        private double width;

        public Rectangle(double length, double width) {
            this.length = length;
            this.width = width;
        }

        @Override
        public double area() {
            return (length * width);
        }
    }


    // Here "CustomRectangle" class is allowed to extend "non-sealed class Rectangle".
    public class CustomRectangle extends Rectangle {
        public CustomRectangle(double length, double width) {
            super(length, width);
        }
    }

    @Test
    public void testCircle() {
        if (verifyNoPropertyViolation()){
            Shape shape = new Circle(5);

            // Test Circle Instance
            assertTrue("",shape instanceof Circle);

            // Test Circle "area"
            assertEquals(Math.PI * 25, shape.area());
        }
    }

    @Test
    public void testSquare() {
        if (verifyNoPropertyViolation()){
            Shape shape = new Square(4);

            // Test Square Instance
            assertTrue("",shape instanceof Square);

            // Test Square "area"
            assertEquals(16, shape.area());
        }
    }

    @Test
    public void testRectangle() {
        if (verifyNoPropertyViolation()) {
            Shape shape = new Rectangle(3, 7);

            // Test Rectangle Instance
            assertTrue("", shape instanceof Rectangle);

            // Test Rectangle "area"
            assertEquals(21, shape.area());
        }
    }

    @Test
    public void testCustomRectangle() {
        if (verifyNoPropertyViolation()){
            Shape shape = new CustomRectangle(4, 5);
            Rectangle rectangle = new CustomRectangle(3,4);

            // Test CustomRectangle Instance
            assertTrue("",shape instanceof CustomRectangle);
            assertTrue("",rectangle instanceof CustomRectangle);

            // Test CustomRectangle "area"
            assertEquals(20, shape.area());
        }
    }
}

[cyrille-artho]

Is there a need to have both Circle and Square in the class hierarchy? They seem to test the same thing. I also think that floating point equivalence can be problematic (e.g., on M chips that don't use strict_fp by default). Can't we remove Circle?

[eklaDFF]

We can remove Circle .

To make symmetry, should I remove Circle from "sealed class" Test too ?

[cyrille-artho]

Yes, you can remove that class everywhere. It is good to test software thoroughly, but if tests are completely redundant, removing them now reduces the burden for code review and maintenance. Here, Circle acts in the exact same way as Square; only the formulas are different. That aspect is not relevant for sealed/non-sealed/final classes as a feature.

[eklaDFF]

package java17;

import gov.nasa.jpf.util.test.TestJPF;
import org.junit.Test;

public class SealedClassTest extends TestJPF {

    // Shape is a "sealed" class, and it allows only "Circle", "Square" and "Rectangle" to extend.
    sealed class Shape permits Square, Rectangle {

    }


    // Here "Square" class is allowed to extend "Shape". Sealed class "Shape" allows "Square" to extends in "permits" clause.
    // But "Square" is "final class" so it cannot be extended by anyone more.
    final class Square extends Shape {

    }


    // Here "Rectangle" class is allowed to extend "Shape". Sealed class "Shape" allows "Rectangle" to extends in "permits" clause.
    // But "Rectangle" is "non-sealed class" so it can be extended by anyone more.
    non-sealed class Rectangle extends Shape {

    }


    // Here "CustomRectangle" class is allowed to extend "non-sealed class Rectangle".
    class CustomRectangle extends Rectangle {

    }

    @Test
    public void testSquareInstance() {
        if (verifyNoPropertyViolation()){
            Shape shape = new Square();
            assertTrue("", shape instanceof Square);
        }
    }

    @Test
    public void testRectangleInstance() {
        if (verifyNoPropertyViolation()){
            Shape shape = new Rectangle();
            assertTrue("", shape instanceof Rectangle);
        }
    }

    @Test
    public void testCustomRectangleInstance() {
        if (verifyNoPropertyViolation()){
            Shape shape = new CustomRectangle();
            assertTrue("", shape instanceof CustomRectangle);
            assertTrue("", shape instanceof Rectangle);
        }
    }
}

package java17;

import gov.nasa.jpf.util.test.TestJPF;
import org.junit.Test;

public class SealedInterfaceTest extends TestJPF {

    // "Shape" is a "sealed" interface, and it allows only "Circle", "Square" and "Rectangle" to implement.
    sealed interface Shape permits Square, Rectangle {
        double area();
    }


    // Here "Square" class is allowed to implement "Shape". Sealed interface "Shape" allows "Square" to implement in "permits" clause.
    // But "Square" is "final class" so it cannot be extended by anyone more.
    final class Square implements Shape {
        private double length;

        public Square(double length){
            this.length = length;
        }

        @Override
        public double area() {
            return (length * length);
        }
    }


    // Here "Rectangle" class is allowed to implement "Shape". Sealed interface "Shape" allows "Rectangle" to implement in "permits" clause.
    // But "Rectangle" is "non-sealed class" so it can be extended by anyone more.
    public non-sealed class Rectangle implements Shape {
        private double length;
        private double width;

        public Rectangle(double length, double width) {
            this.length = length;
            this.width = width;
        }

        @Override
        public double area() {
            return (length * width);
        }
    }


    // Here "CustomRectangle" class is allowed to extend "non-sealed class Rectangle".
    public class CustomRectangle extends Rectangle {
        public CustomRectangle(double length, double width) {
            super(length, width);
        }
    }

    @Test
    public void testSquare() {
        if (verifyNoPropertyViolation()){
            Shape shape = new Square(4);

            // Test Square Instance
            assertTrue("",shape instanceof Square);

            // Test Square "area"
            assertEquals(16, shape.area());
        }
    }

    @Test
    public void testRectangle() {
        if (verifyNoPropertyViolation()) {
            Shape shape = new Rectangle(3, 7);

            // Test Rectangle Instance
            assertTrue("", shape instanceof Rectangle);

            // Test Rectangle "area"
            assertEquals(21, shape.area());
        }
    }

    @Test
    public void testCustomRectangle() {
        if (verifyNoPropertyViolation()){
            Shape shape = new CustomRectangle(4, 5);
            Rectangle rectangle = new CustomRectangle(3,4);

            // Test CustomRectangle Instance
            assertTrue("",shape instanceof CustomRectangle);
            assertTrue("",rectangle instanceof CustomRectangle);

            // Test CustomRectangle "area"
            assertEquals(20, shape.area());
        }
    }
}

Should create a PR now ?

[cyrille-artho]

Yes, please do so.

[eklaDFF]

#486

[cyrille-artho]

Thanks!