Jump to content
xau

Spec# - [Owned] attribute

Recommended Posts

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.  :cheesygrin:

Share this post


Link to post
Share on other sites
will09

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

e k numka ouvi falar dixo  :wallbash:

PEACE  :smoke:

Share this post


Link to post
Share on other sites
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;
}
}

Share this post


Link to post
Share on other sites
will09

Bgd plo esclarecimento foi novidade para mim!  :)

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

PEACE  :smoke:

Share this post


Link to post
Share on other sites
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.

Share this post


Link to post
Share on other sites

Create an account or sign in to comment

You need to be a member in order to leave a comment

Create an account

Sign up for a new account in our community. It's easy!

Register a new account

Sign in

Already have an account? Sign in here.

Sign In Now

×
×
  • Create New...

Important Information

By using this site you accept our Terms of Use and Privacy Policy. We have placed cookies on your device to help make this website better. You can adjust your cookie settings, otherwise we'll assume you're okay to continue.