specification ContactsWithLogic

// Resource declaration
resource Contact {
	pred hasId(integer),
	pred hasName(string),
	pred hasEmail(string),
	pred hasBirthDate(integer)
}

resource ContactList {
	pred contains(Contact)
}

// Type declaration
type ContactRep = (cr: { 
	id: integer,
	name: (x : string where x.length > 2),	
	email: (e: string where contains(["@"],e)),
	birthDate: integer,
	registerDate: integer,
	newsSubscriptionType: (subType: string where subType in ["ANUAL"] || subType in ["SEMANAL"] || subType in ["DIARIO"]),
	newsSubscriptionWhen: integer
} where 
	(cr.newsSubscriptionWhen > 0) &&
	(cr.birthDate < cr.registerDate) &&
	(cr.newsSubscriptionType == "ANUAL" => cr.newsSubscriptionWhen <= 365) &&
	(cr.newsSubscriptionType == "SEMANAL" => cr.newsSubscriptionWhen <= 7) &&
	(cr.newsSubscriptionType == "DIARIO" => cr.newsSubscriptionWhen <= 24)
)

type ContactPostData = (cpd: {
	id: integer,
	name: (x : string where x.length > 2),	
	email: (e: string where contains(["@"],e)),
	birthDate: integer,
	newsSubscriptionType: (subType: string where subType in ["ANUAL"] || subType in ["SEMANAL"] || subType in ["DIARIO"]),
	newsSubscriptionWhen: integer
} where
	(cpd.newsSubscriptionWhen > 0) &&
	(cpd.newsSubscriptionType == "ANUAL" => cpd.newsSubscriptionWhen <= 365) &&
	(cpd.newsSubscriptionType == "SEMANAL" => cpd.newsSubscriptionWhen <= 7) &&
	(cpd.newsSubscriptionType == "DIARIO" => cpd.newsSubscriptionWhen <= 24)
)

type ContactPutData = (cpd: {
	name: (x : string where x.length > 2),	
	email: (e: string where contains(["@"],e)),
	newsSubscriptionType: (subType: string where subType in ["ANUAL"] || subType in ["SEMANAL"] || subType in ["DIARIO"]),
	newsSubscriptionWhen: integer
} where
	(cpd.newsSubscriptionWhen > 0) &&
	(cpd.newsSubscriptionType == "ANUAL" => cpd.newsSubscriptionWhen <= 365) &&
	(cpd.newsSubscriptionType == "SEMANAL" => cpd.newsSubscriptionWhen <= 7) &&
	(cpd.newsSubscriptionType == "DIARIO" => cpd.newsSubscriptionWhen <= 24)
)

type ContactListRep = {
	contacts: ContactRep[]
}

/**
 * Link representation with resource, defining a predicate
 */
contact:ContactRep represents Contact{
	hasId(var1) => var1 == contact.id,
	hasName(var1) => var1 == contact.name,
	hasEmail(var1) => var1 == contact.email,
	hasBirthDate(var1) => var1 == contact.birthDate
}

contactList:ContactListRep represents ContactList{
	contains(contact) => (exists i:(x: integer where x >= 0 && x < contactList.contacts.length) . contact.hasId(contactList.contacts[i].id))
}

// Constant declarations
def SUCCESS = 200
def CREATED = 201
def CONFLICT = 409

// Axioms
{
	true
}
	GET /contacts
{
	response.code == SUCCESS &&
	response in {body: ContactListRep} &&&
	(exists l: ContactList .
		response.body representationof l
	)
}

{   
	request in {body: ContactPostData} &&&
    (forall c: Contact . !c.hasId(request.body.id))
}
	POST /contacts
{   
	response.code == CREATED &&
	response in {body: ContactRep, header: {Location: URI}} &&& 
	(exists l: ContactList .
		(exists c: Contact . 
			l.contains(c) &&
			response.body representationof c && 
			response.header.Location uriof c &&
			c.hasId(response.body.id) &&
			c.hasName(response.body.name) &&
			c.hasEmail(response.body.email) &&
			c.hasBirthDate(response.body.birthDate)
		)
	)
}

// add contact, CONFLICT
{
	request in {body: ContactPostData} &&&
	(exists c: Contact . c.hasId(request.body.id))
}
	POST /contacts
{
    response.code == CONFLICT
}

// update contact, SUCCESS
{
	request in {body: ContactPutData, template:{id:integer}} &&&
	(exists c: Contact . c.hasId(request.template.id))
}
	PUT /contacts/{id}
{
	response.code == SUCCESS &&
	response in {body: ContactRep} &&&
	(exists l: ContactList .
		(exists c: Contact . 
			l.contains(c) &&
			response.body representationof c &&
			c.hasId(response.body.id) &&
			c.hasName(response.body.name) &&
			c.hasEmail(response.body.email) &&
			c.hasBirthDate(response.body.birthDate)
		)
	)
}