Spec# - [Owned] attribute

[xau]

Boas.

Sei à partida que vai ser difícil de obter uma resposta, considerando que o Spec# é uma linguagem muito recente... No entanto, aqui vai a minha questão.

O que eu quero é declarar um objecto como owned pelo seu master. O que me acontece é que quando escrevo [Owned], o Visual Studio não reconhece este atributo.

O erro aponta para um esquecimento de uma directiva 'using'. Já experimentei com o 'Microsoft.Contracts', namespace que inclui outros atributos do Spec# como o [Pure], o [Confined] e outros, mas parece que o [Owned] não se encontra no mesmo sítio. Já pesquisei na net e aparecem vários exemplos com o [Owned]. Nunca dizem é onde é que eu o posso ir buscar.  😉

Bem, se souberem alguma coisa sobre isto... Façam o favor.  😁

[will09]

Podias dar uma dicas ai ao pexoal sobre o k é o Spec#??

e k numka ouvi falar dixo 

PEACE  :smoke:

[xau]

O Spec# é mais uma linguagem que faz parte da ferramenta .NET e vem extender o C#, introduzindo as especificações para programação por contratos (design by contracts).

  - tipos não nulos

  - contratos de métodos: pré e pós-condições, frame conditions

  - contratos de objectos/classes: invariantes

  - conceito de ownership (em que um objecto que esteja agregado ao seu master, lhe pertence e pode ser modificado por ele)

O que é a programação por contratos? http://en.wikipedia.org/wiki/Design_by_contract

Um paradigma introduzido pela linguagem Eiffel, mais ou menos como o JML para o Java (só para citar um exemplo), que permite definir condições que devem ser satisfeitas pelos vários componentes de um programa orientado a objectos. Existem vários tipos de condições, das quais se destacam:

  - pré-condições: condições que devem ser satisfeitas pelo cliente na chamada a um método; são por isso da responsabilidade do cliente (cliente este que tanto pode ser o utilizador final, como

    outro software ou mesmo o nosso próprio software, que usam o nosso método);

  - pós-condições: condições que devem ser satisfeitas pela nossa implementação, no caso de a pré-condição ter sido satisfeita à entrada no método.

  - invariantes: condições que devem ser satisfeitas em qualquer momento da nossa implementação (um comprimento ser sempre maior ou igual a zero, por exemplo);

  - ...

As especificações permitem também atribuir responsabilidades em caso de erro. No fundo o Spec# é uma contribuição para a construção de código mais fiável.

Mas esta é uma linguagem que ainda se encontra em estudo e desenvolvimento, algumas das suas potencialidades ainda não têm maturidade suficiente para serem usadas na sua plenitude. Outro pormenor importante é que o Spec# (linguagem) ainda não tem documentação - manual de referência, etc. O que se encontra são apenas papers dos autores, apresentações de colaboradores e coisas do género. Poderão saber mais no site oficial: http://research.microsoft.com/specsharp/

Exemplo de código em Spec#:

using System;
using System.Collections.Generic;
using System.Compiler.Contracts;
using System.Compiler.Guards;
using System.Runtime;
using System.Guards;
using Microsoft.Contracts;

public class Turma {
private Aluno[]! alunos;       //tipo não nulo (nome da classe + '!')
private string nome;
private int tamanho;

invariant tamanho == alunos.Length;            //invariante

public Turma(string! n)
	requires n != "";            //pré-condição
{
	alunos = new Aluno[0];
	base();
	nome = n;
}

public Turma(Aluno[]! a, string! n)
	requires n != "";            //pré-condição
{
	alunos = a;
	base();
	nome = n;
}

        //'Pure' - custom attribute que indica que o referido método não tem efeitos secundários e pode, portanto, ser usado como parte de uma especificação
        //muito útil, especialmente nos casos em que temos atributos privados e não podemos mencioná-los nos contratos (para não violar o princípio de information hiding)
[Pure] public Aluno[]! getAlunos() {
	return alunos;
}

[Pure] public string! getNome() {
	return nome;
}

[Pure] public int getTamanho() {
	return tamanho;
}

public void setAlunos(Aluno[]! a)
	modifies this.Turma;          //frame condition
	ensures getAlunos().Length == a.Length;         //pós-condição
{
	expose(this) {
		alunos = a;
		tamanho = alunos.Length;
	}
}

public void setNome(string! n)
	requires n != "";        //pré-condição
	modifies this.Turma;      //frame condition
	ensures getNome().Equals(n);      //pós-condição
{
	nome = n;
}

[Pure] public Aluno getAlunoPos(int pos)
	requires pos >= getTamanho();     //pré-condição
{
	return alunos[pos];
}

public void addAluno(Aluno! a)
	ensures getAlunos().Length == old(getAlunos().Length) + 1;       //pós-condição
	ensures getTamanho() == old(getTamanho()) + 1;        //pós-condição
{
	int i;
	int newLength;
	Aluno[]! temp;

	newLength = alunos.Length+1;

	temp = new Aluno[newLength];

	for (i=0; i<alunos.Length; i++) {
		temp[i] = alunos[i];
	}

	temp[i] = a;

	Console.WriteLine("\n\n\nVou adicionar o aluno " + a.getNome());

	//exposição de um objecto (altura em que o invariante pode ser violado, tendo que
	//se verificar novamente no final do bloco 'expose'
	expose(this){			
		alunos = temp;
		tamanho = alunos.Length;
		tamanho++;
		Console.WriteLine("O invariante e' valido? " + this.InvariantHolds());
	}
	Console.WriteLine("Adicionei o aluno " + a.getNome());
	Console.WriteLine("O invariante e' valido? " + this.InvariantHolds());
}

public override string ToString() {
	string s = "";

	foreach(Aluno a in alunos)
	if (a != null)
		s += a.ToString();

	return s;
}
}

[will09]

Bgd plo esclarecimento foi novidade para mim!  🙂

O codigo e igualzinho ao C# variando apenas as condições! Inda n tinha "ouvisto"  😁  falar disto =)

PEACE  :smoke:

[xau]

Bem, para mim também é novidade. Tive que fazer um trabalho sobre o Spec# para uma cadeira, no qual tive que dar uma aula de 2 horas. Nem sequer C# sabia, mas com bons conhecimentos de Java, a adaptação é bastante rápida. Já conhecia a programação por contratos, mas este trabalho permitiu-me aprender bastante sobre as suas potencialidades. Haverá sempre resistência à mudança de comportamento por parte dos designers de software e dos programadores, no entanto os clientes são cada vez mais exigentes e o desenvolvimento de software mais fiável e robusto é o futuro. Também é de salientar que este tipo de programação nos ajuda, como designers e programadores, a definir em concreto quais são as nossas responsabilidades e quais são as do cliente, no que toca ao comportamento do software. Isso torna a atribuição de responsabilidades em caso de erro muito mais transparente. É claro que estamos a exigir mais de nós próprios, mas só assim podemos evoluir.