001package components.queue; 002 003import java.util.Comparator; 004 005/** 006 * {@code QueueKernel} enhanced with secondary methods. 007 * 008 * @param <T> 009 * type of {@code Queue} entries 010 * @mathdefinitions {@code 011 * IS_TOTAL_PREORDER ( 012 * r: binary relation on T 013 * ) : boolean is 014 * for all x, y, z: T 015 * ((r(x, y) or r(y, x)) and 016 * (if (r(x, y) and r(y, z)) then r(x, z))) 017 * 018 * IS_SORTED ( 019 * s: string of T, 020 * r: binary relation on T 021 * ) : boolean is 022 * for all x, y: T where (<x, y> is substring of s) (r(x, y)) 023 * } 024 */ 025public interface Queue<T> extends QueueKernel<T> { 026 027 /** 028 * Reports the front of {@code this}. 029 * 030 * @return the front entry of {@code this} 031 * @aliases reference returned by {@code front} 032 * @requires {@code this /= <>} 033 * @ensures {@code <front> is prefix of this} 034 */ 035 T front(); 036 037 /** 038 * Replaces the front of {@code this} with {@code x}, and returns the old 039 * front. 040 * 041 * @param x 042 * the new front entry 043 * @return the old front entry 044 * @aliases reference {@code x} 045 * @updates this 046 * @requires {@code this /= <>} 047 * @ensures {@code 048 * <replaceFront> is prefix of #this and 049 * this = <x> * #this[1, |#this|) 050 * } 051 */ 052 T replaceFront(T x); 053 054 /** 055 * Concatenates ("appends") {@code q} to the end of {@code this}. 056 * 057 * @param q 058 * the {@code Queue} to be appended to the end of {@code this} 059 * @updates this 060 * @clears q 061 * @ensures this = #this * #q 062 */ 063 void append(Queue<T> q); 064 065 /** 066 * Reverses ("flips") {@code this}. 067 * 068 * @updates this 069 * @ensures this = rev(#this) 070 */ 071 void flip(); 072 073 /** 074 * Sorts {@code this} according to the ordering provided by the 075 * {@code compare} method from {@code order}. 076 * 077 * @param order 078 * ordering by which to sort 079 * @updates this 080 * @requires IS_TOTAL_PREORDER([relation computed by order.compare method]) 081 * @ensures <pre> 082 * perms(this, #this) and 083 * IS_SORTED(this, [relation computed by order.compare method]) 084 * </pre> 085 */ 086 void sort(Comparator<T> order); 087 088 /** 089 * Rotates {@code this}. 090 * 091 * @param distance 092 * distance by which to rotate 093 * @updates this 094 * @ensures {@code 095 * if #this = <> then 096 * this = #this 097 * else 098 * this = #this[distance mod |#this|, |#this|) * #this[0, distance mod |#this|) 099 * } 100 */ 101 void rotate(int distance); 102 103}