Winx: Software Specification Language

Welcome to Winx, a powerful language for defining software specifications in a clear and structured manner. This README provides an overview of Winx and its features.

Overview

Winx is a domain-specific language (DSL) specifically designed for writing software specifications. It offers a concise syntax for describing both functional and non-functional requirements, interfaces, packages, and more.

Key Features

Clear Syntax

• Winx provides a clean and easy-to-understand syntax for defining various elements of software specifications.

Hierarchical Structure

• Specifications can be organized hierarchically into packages, interfaces, and specifications, providing a clear structure for complex software systems.

Non-Functional Requirements

• Winx allows you to define non-functional requirements such as performance, security, and reliability constraints using clear and concise syntax.

Functional Requirements

• You can specify functional requirements, including input parameters, output types, and implementation details, using intuitive syntax.

Importance Levels

• Winx supports specifying the importance level of requirements, allowing you to prioritize critical functionalities over optional ones.

Access Modifiers

• Access modifiers such as public, protected, private, and default can be applied to interfaces and functions, enabling fine-grained control over visibility and accessibility.

Comments

• Winx supports both single-line and block comments, helping you document your specifications effectively.

Example

package Database {
    interface Database {
        public GetUserList(FLOAT[] x, STRING ag) {
            @ExecTime: "10s";
            @MaxReturnVals: "10s";
            return INT x;
        }
    }

    specification DatabaseAccess implements Database {
        critical DatabaseAccessMember {
            optional @UserHasAdminAccess;
            critical @UserIsNotBanned;
            result optional DatabaseAdminPanel;
            result critical DatabaseVisualizerPanel;
            result Clock;
        }

        public GetUserList(FLOAT[] x, STRING ag) implements DatabaseAccessImpl {
            @ExecTime: "10s";
            @MaxReturnVals: "10s";
            return INT x;
        }
    }
}