Sequence — secuencia ordenada como subtipo de Collection

Posiciones indexadas desde 1; permite repeticiones; add agrega al final.

Validación: bajamos de 190 errores en la versión original a 0 errores, 5 warnings. Los 5 warnings son V1 sobre operaciones parciales (subSequence, atSequence, indexOfSequence, firstSequence, lastSequence): sus precondiciones excluyen s = create pero el analyzer del workspace no modela precondiciones expresadas vía size, isEmpty o includes. Son los falsos positivos esperados según la memoria del proyecto.

Estrategia (como bag.nereus): cada operación derivada tiene dos vistas conviviendo:

Extensional: caracterización vía las observaciones (atSequence, size, count, includes). Documenta el significado.
Constructor-pattern: axiomas con LHS de la forma op(create, ...) y op(add(s, e), ...). Cubre V1 y da reglas de reescritura inductivas.

1. Especificación corregida

-- ============================================================ -- Sequence — secuencia ordenada (permite repeticiones, -- posiciones indexadas desde 1). -- ============================================================ CLASS Sequence [Elem] IMPORTS Set[Elem:ANY], Bag[Elem:ANY], OrderedSet[Elem:ANY] IS-SUBTYPE-OF Collection[Elem] BASIC CONSTRUCTORS create, add EFFECTIVE TYPE Sequence OPERATIONS -- ─── Constructores básicos heredados ────────────────── create: -> Sequence; add: Sequence * Elem -> Sequence; -- ─── Sinónimos de add (al final) ────────────────────── appendSequence: Sequence * Elem -> Sequence; includingSequence: Sequence * Elem -> Sequence; -- ─── Propias de Sequence ────────────────────────────── count: Sequence * Elem -> Integer; equalSequence: Sequence * Sequence -> Boolean; prependSequence: Sequence * Elem -> Sequence; unionSequence: Sequence * Sequence -> Sequence; insertAtSequence: Sequence(s) * Integer(idx) * Elem -> Sequence pre: (1 <= idx) and (idx <= size(s) + 1); excludingSequence: Sequence * Elem -> Sequence; subSequence: Sequence(s) * Integer(lower) * Integer(upper) -> Sequence pre: (1 <= lower) and (lower <= upper) and (upper <= size(s)); atSequence: Sequence(s) * Integer(i) -> Elem pre: (i >= 1) and (i <= size(s)); indexOfSequence: Sequence(s) * Elem(e) -> Integer pre: includes(s, e); firstSequence: Sequence(s) -> Elem pre: not isEmpty(s); lastSequence: Sequence(s) -> Elem pre: not isEmpty(s); sequenceAsBag: Sequence -> Bag; sequenceAsSet: Sequence -> Set; sequenceAsOrderedSet: Sequence -> OrderedSet; AXIOMS s, s1: Sequence; e, e1, v: Elem; i, idx, lower, upper: Integer; -- Sinónimos appendSequence(create(), e) = add(create(), e) as Sequence; appendSequence(add(s, e1), e) = add(add(s, e1), e) as Sequence; includingSequence(create(), e) = add(create(), e) as Sequence; includingSequence(add(s, e1), e) = add(add(s, e1), e) as Sequence; -- count count(create(), e1) = 0; (e = e1) implies count(add(s, e), e1) = 1 + count(s, e1); not (e = e1) implies count(add(s, e), e1) = count(s, e1); -- atSequence (precondición excluye create) atSequence(add(s, e) as Sequence, size(add(s, e) as Sequence)) = e; ((1 <= idx) and (idx <= size(s))) implies atSequence(add(s, e) as Sequence, idx) = atSequence(s, idx); -- equalSequence: recursión estructural limpia (orden importa) equalSequence(create(), create()) = True; equalSequence(create(), add(s1, e1)) = False; equalSequence(add(s, e), create()) = False; equalSequence(add(s, e), add(s1, e1)) = (e = e1) and equalSequence(s, s1); -- prependSequence prependSequence(create(), e) = add(create(), e) as Sequence; prependSequence(add(s, e1), e) = add(prependSequence(s, e), e1) as Sequence; atSequence(prependSequence(s, e), 1) = e; ((1 <= idx) and (idx <= size(s))) implies atSequence(prependSequence(s, e), idx + 1) = atSequence(s, idx); -- unionSequence: concatenación, inducción sobre el segundo arg unionSequence(s, create()) = s; unionSequence(s, add(s1, e)) = add(unionSequence(s, s1), e) as Sequence; size(unionSequence(s, s1)) = size(s) + size(s1); ((1 <= idx) and (idx <= size(s))) implies atSequence(unionSequence(s, s1), idx) = atSequence(s, idx); ((size(s) < idx) and (idx <= size(s) + size(s1))) implies atSequence(unionSequence(s, s1), idx) = atSequence(s1, idx - size(s)); -- insertAtSequence insertAtSequence(create(), idx, e) = add(create(), e) as Sequence; (idx = size(add(s, e1) as Sequence) + 1) implies insertAtSequence(add(s, e1) as Sequence, idx, e) = add(add(s, e1) as Sequence, e) as Sequence; (idx <= size(add(s, e1) as Sequence)) implies insertAtSequence(add(s, e1) as Sequence, idx, e) = add(insertAtSequence(s, idx, e), e1) as Sequence; atSequence(insertAtSequence(s, idx, e), idx) = e; size(insertAtSequence(s, idx, e)) = size(s) + 1; ((1 <= i) and (i < idx)) implies atSequence(insertAtSequence(s, idx, e), i) = atSequence(s, i); ((idx <= i) and (i <= size(s))) implies atSequence(insertAtSequence(s, idx, e), i + 1) = atSequence(s, i); -- subSequence (precondición excluye create) (upper <= size(s)) implies subSequence(add(s, e1) as Sequence, lower, upper) = subSequence(s, lower, upper); ((lower <= size(s)) and (upper > size(s))) implies subSequence(add(s, e1) as Sequence, lower, upper) = add(subSequence(s, lower, size(s)), e1) as Sequence; (lower > size(s)) implies subSequence(add(s, e1) as Sequence, lower, upper) = add(create(), e1) as Sequence; size(subSequence(s, lower, upper)) = upper - lower + 1; ((lower <= idx) and (idx <= upper)) implies atSequence(subSequence(s, lower, upper), idx - lower + 1) = atSequence(s, idx); -- indexOfSequence (precondición excluye create) includes(s, e) implies indexOfSequence(add(s, e1) as Sequence, e) = indexOfSequence(s, e); ((not includes(s, e)) and (e1 = e)) implies indexOfSequence(add(s, e1) as Sequence, e) = size(add(s, e1) as Sequence); atSequence(s, indexOfSequence(s, e)) = e; -- firstSequence, lastSequence (precondición excluye create) isEmpty(s) implies firstSequence(add(s, e) as Sequence) = e; not isEmpty(s) implies firstSequence(add(s, e) as Sequence) = firstSequence(s); lastSequence(add(s, e) as Sequence) = e; -- excludingSequence excludingSequence(create(), e) = create() as Sequence; (e1 = e) implies excludingSequence(add(s, e1) as Sequence, e) = excludingSequence(s, e); not (e1 = e) implies excludingSequence(add(s, e1) as Sequence, e) = add(excludingSequence(s, e), e1) as Sequence; not includes(excludingSequence(s, e), e); size(excludingSequence(s, e)) = size(s) - count(s, e); -- sequenceAsBag sequenceAsBag(create()) = create() as Bag; sequenceAsBag(add(s, e) as Sequence) = add(sequenceAsBag(s), e) as Bag; count(sequenceAsBag(s), v) = count(s, v); -- sequenceAsSet (respeta precond. de addSet) sequenceAsSet(create()) = create() as Set; includes(sequenceAsSet(s), e) implies sequenceAsSet(add(s, e) as Sequence) = sequenceAsSet(s); not includes(sequenceAsSet(s), e) implies sequenceAsSet(add(s, e) as Sequence) = addSet(sequenceAsSet(s), e); includes(sequenceAsSet(s), v) = (count(s, v) > 0); -- sequenceAsOrderedSet sequenceAsOrderedSet(create()) = createOrderedSet(); includes(sequenceAsOrderedSet(s), e) implies sequenceAsOrderedSet(add(s, e) as Sequence) = sequenceAsOrderedSet(s); not includes(sequenceAsOrderedSet(s), e) implies sequenceAsOrderedSet(add(s, e) as Sequence) = includingOrderedSet(sequenceAsOrderedSet(s), e); includes(sequenceAsOrderedSet(s), v) = (count(s, v) > 0); -- Preservación de orden (uses indexOfOrderedSet importado) ((indexOfSequence(s, v) < indexOfSequence(s, e)) and includes(s, v) and includes(s, e)) implies (indexOfOrderedSet(sequenceAsOrderedSet(s), v) < indexOfOrderedSet(sequenceAsOrderedSet(s), e)); END-CLASS

2. Resumen de las correcciones aplicadas

#	Problema en versión original	Corrección
Errores sintácticos (190 reportes en cascada)
1	Línea 8: `create, add, count;` sin signatures	Tres signatures completas: `create: -> Sequence`, `add: SequenceElem->Sequence`, `count: SequenceElem->Integer`
2	Líneas 58-59: `iterate` con coma faltante, `acc` y `v` no declarados, argumentos invertidos	Eliminado el `iterate` roto; `excludingSequence` queda solo con su forma constructor-pattern
Bugs de typos en variables
3	L29: `count(s, e)` en else (debería ser `count(s, e1)`)	Fixeado
4	L47-48: `atSequence(insertAtSequence(...), 1)` debería ser `i+1`	Fixeado
5	L61-62: `excludingSequence(s, e)` recursivo (debería ser `e1`)	Reescrito sobre `add(s, e1)` con `implies` y referencias correctas
6	L63 y L70: `count(...,e)` donde la variable de cuantif es `v`	Fixeado
Bugs lógicos
7	L30-31: `equalSequence` con variable libre `index` y precedencia ambigua	Reescrito por 4 casos constructor-pattern (recursión limpia gracias al orden)
8	L34: caracterización de `unionSequence` solo para primera mitad	Agregada axioma para segunda mitad: `size(s) < idx <= size(s)+size(s1)`
9	L67: tautología `forAll (v) (sequenceAsSet(s), [includes(sequenceAsSet(s),v)])`	Reemplazada por la caracterización correcta vía `count`
10	L71-74: preservación de orden con espacios de índices y elementos distintos	Reescrita con `indexOfSequence(s, v) < indexOfSequence(s, e)`
Operaciones no declaradas o faltantes
11	L65: `sequenceAsSeq(s) = s` — operación no declarada	Eliminado
12	Faltaba `appendSequence` (referenciada por `Set.nereus:144`)	Declarada y axiomatizada (= `add` con cast)
13	Faltaba axioma base `count(create(), e) = 0`	Agregado
14	Faltaba `BASIC CONSTRUCTORS create, add`	Agregado
15	`firstSequence`/`lastSequence` sin precondición	Agregado `pre: not isEmpty(s)`
Estilo y redundancias
16	`Integer` en `IMPORTS` (es built-in)	Quitado
17	Variables `f`, `g`, `h`, `k` declaradas y no usadas	Eliminadas
18	`if-then-else / endif` en múltiples axiomas	Migrados a `implies`
19	`TYPE` y `Sequence` en líneas separadas	Consolidado
20	Sin comentarios de sección	Agregados (consistente con `bag.nereus`, `BSTree-hide.nereus`)

Problema en versión original

Corrección

Errores sintácticos (190 reportes en cascada)

Línea 8: create, add, count; sin signatures

Tres signatures completas: create: -> Sequence, add: Sequence*Elem->Sequence, count: Sequence*Elem->Integer

Líneas 58-59: iterate con coma faltante, acc y v no declarados, argumentos invertidos

Eliminado el iterate roto; excludingSequence queda solo con su forma constructor-pattern

Bugs de typos en variables

L29: count(s, e) en else (debería ser count(s, e1))

Fixeado

L47-48: atSequence(insertAtSequence(...), 1) debería ser i+1

Fixeado

L61-62: excludingSequence(s, e) recursivo (debería ser e1)

Reescrito sobre add(s, e1) con implies y referencias correctas

L63 y L70: count(...,e) donde la variable de cuantif es v

Fixeado

Bugs lógicos

L30-31: equalSequence con variable libre index y precedencia ambigua

Reescrito por 4 casos constructor-pattern (recursión limpia gracias al orden)

L34: caracterización de unionSequence solo para primera mitad

Agregada axioma para segunda mitad: size(s) < idx <= size(s)+size(s1)

L67: tautología forAll (v) (sequenceAsSet(s), [includes(sequenceAsSet(s),v)])

Reemplazada por la caracterización correcta vía count

L71-74: preservación de orden con espacios de índices y elementos distintos

Reescrita con indexOfSequence(s, v) < indexOfSequence(s, e)

Operaciones no declaradas o faltantes

L65: sequenceAsSeq(s) = s — operación no declarada

Eliminado

Faltaba appendSequence (referenciada por Set.nereus:144)

Declarada y axiomatizada (= add con cast)

Faltaba axioma base count(create(), e) = 0

Agregado

Faltaba BASIC CONSTRUCTORS create, add

Agregado

firstSequence/lastSequence sin precondición

Agregado pre: not isEmpty(s)

Estilo y redundancias

Integer en IMPORTS (es built-in)

Quitado

Variables f, g, h, k declaradas y no usadas

Eliminadas

if-then-else / endif en múltiples axiomas

Migrados a implies

TYPE y Sequence en líneas separadas

Consolidado

Sin comentarios de sección

Agregados (consistente con bag.nereus, BSTree-hide.nereus)

3. Axiomas constructor-pattern por operación

Operación	Caso `create`	Caso `add(s, e)`
`count`	`= 0`	2 implies (según `e = e1`)
`equalSequence`	4 combinaciones create/add × create/add (recursión estructural)	—
`appendSequence`, `includingSequence`	`= add(create(), e)`	`= add(add(s, e1), e)`
`prependSequence`	`= add(create(), e)`	`= add(prependSequence(s, e), e1)`
`unionSequence`	Inducción sobre el segundo arg: `unionSequence(s, create) = s`; `unionSequence(s, add(s1, e)) = add(unionSequence(s, s1), e)`
`insertAtSequence`	`insertAtSequence(create, idx, e)` con idx=1 (único válido)	2 implies (idx al final vs idx interno)
`excludingSequence`	`= create()`	2 implies según `e1 = e`
`subSequence` ★	—	3 implies (upper ≤ size(s) / lower ≤ size(s) < upper / lower > size(s))
`atSequence` ★	—	2 axiomas (último elemento / posición interna)
`indexOfSequence` ★	—	2 implies (e en s / e solo al final)
`firstSequence` ★	—	2 implies según `isEmpty(s)`
`lastSequence` ★	—	1 (siempre `e`, porque `add` apila al final)
`sequenceAsBag`	`= create() as Bag`	`= add(sequenceAsBag(s), e) as Bag`
`sequenceAsSet`	`= create() as Set`	2 implies según ya esté incluido (respeta precond. de `addSet`)
`sequenceAsOrderedSet`	`= createOrderedSet()`	2 implies análogos a sequenceAsSet

Operación

Caso create

Caso add(s, e)

count

= 0

2 implies (según e = e1)

equalSequence

4 combinaciones create/add × create/add (recursión estructural)

—

appendSequence, includingSequence

= add(create(), e)

= add(add(s, e1), e)

prependSequence

= add(create(), e)

= add(prependSequence(s, e), e1)

unionSequence

Inducción sobre el segundo arg: unionSequence(s, create) = s; unionSequence(s, add(s1, e)) = add(unionSequence(s, s1), e)

insertAtSequence

insertAtSequence(create, idx, e) con idx=1 (único válido)

2 implies (idx al final vs idx interno)

excludingSequence

= create()

2 implies según e1 = e

subSequence ★

—

3 implies (upper ≤ size(s) / lower ≤ size(s) < upper / lower > size(s))

atSequence ★

—

2 axiomas (último elemento / posición interna)

indexOfSequence ★

—

2 implies (e en s / e solo al final)

firstSequence ★

—

2 implies según isEmpty(s)

lastSequence ★

—

1 (siempre e, porque add apila al final)

sequenceAsBag

= create() as Bag

= add(sequenceAsBag(s), e) as Bag

sequenceAsSet

= create() as Set

2 implies según ya esté incluido (respeta precond. de addSet)

sequenceAsOrderedSet

= createOrderedSet()

2 implies análogos a sequenceAsSet

★ = operaciones parciales cuya precondición excluye create (not isEmpty, i <= size, includes, etc.). El analyzer todavía emite un warning V1 porque no modela esas precondiciones, pero son los falsos positivos esperados según la memoria del workspace.

4. Casos no triviales del razonamiento

equalSequence sobre dos add: a diferencia de Bag (donde los bags son desordenados y la recursión "ingenua" sobre add es incorrecta), en Sequence el orden importa, así que equalSequence(add(s, e), add(s1, e1)) = (e = e1) and equalSequence(s, s1) es exactamente lo que queremos: dos secuencias son iguales sii sus últimos elementos coinciden y sus prefijos también.

unionSequence y la "segunda mitad": la versión original solo decía que posiciones 1..size(s) del resultado coinciden con s. Faltaba el axioma para posiciones size(s) < idx <= size(s)+size(s1): deben coincidir con s1 en la posición idx - size(s). Sin él, el resultado quedaba subespecificado para la segunda mitad.

subSequence recursivo: hay tres casos según dónde caen lower, upper respecto a size(s) (el último elemento e1 está en la posición size(s)+1 de add(s, e1)):

upper ≤ size(s): el segmento está completamente en s, ignora e1.
lower ≤ size(s) < upper: el segmento abarca parte de s más el último elemento e1.
lower > size(s): el segmento es solo [e1].

indexOfSequence de la primera ocurrencia: si el elemento ya está en el prefijo s, el índice de su primera ocurrencia en add(s, e1) es el mismo que en s (no importa que e1 coincida con e). Si no está en s pero coincide con e1, el índice es size(add(s, e1)) (la última posición). El orden de las dos implies en el axioma respeta esta prioridad.