A web-based social environment for Alloy

Abstract

Alloy is a declarative specification language which describes rules and complex structural behaviors. Alloy Analyzer is used to analyze this specifications, this tool generates concrete instances from the invariants specified in a model, it simulates sequences of defined operations and verifies whether properties introduced are valid or not. Currently, the tool is available as a runnable .jar and it contains a trivial GUI to interact with it. Being such, it requires JAVA installed. It’s in the best interest of the community to achieve and easier access to this tool through a web platform that shall support it in real time and also allow sharing models developed in it by users. Formal methods of software development are growing and they would also benefit from the constructive feedback obtained through this platform regarding the Alloy language/tool.

Alloy é uma linguagem de especificação declarativa que descreve regras e comportamentos de estruturas complexas. Para analisar estas especificações, utiliza-se o Alloy Analyzer, uma ferramenta que gera instâncias concretas a partir dos invariantes especificados num modelo, simula sequências de operações definidas e verifica se as propriedades introduzidas são satisfeitas. Atualmente, a ferramenta está disponível sob a forma de um .jar executável e contém uma GUI trivial para a sua utilização, requerendo assim o respetivo download e instalação do software adicional JAVA até estar operacional. É do interesse da comunidade conseguir um acesso facilitado a esta ferramenta através de uma plataforma web que a suporta em tempo real e permite a partilha simplificada de trabalhos elaborados. Também seria uma mais valia para os métodos formais na produção de software, que se encontram em constante crescimento, a extração de informação estatística acerca da utilização desta plataforma. Daqui poderia obter-se um feedback positivo face aos prós e contras da linguagem/ferramenta.