f

#### SPARK left/right shift.

Hi.

What's the "correct" way to get access to left/right shift operations
for modular types in SPARK? I see from the Checker manual that
the proof language is capable of modelling them but then I also see
that the Interfaces package isn't predefined.

 0
xorquewasp (64)
7/21/2009 9:07:40 AM
comp.lang.ada 8774 articles. 2 followers.

8 Replies
789 Views

Similar Articles

[PageSpeed] 58

On Jul 21, 10:07=A0am, xorque <xorquew...@googlemail.com> wrote:
> Hi.
>
> What's the "correct" way to get access to left/right shift operations
> for modular types in SPARK?

The standard shift/rotate functions in Interfaces
are overloaded, so not legal SPARK.  The way round this is
to declare a "shadow" package that de-overloads them for SPARK.
I'll post an example of how to do it in a minute...
- Rod

 0
7/21/2009 9:21:38 AM
OK - it's done as follows.  We create a SPARK "shadow" specification
of
package Interfaces and a new package SPARK_Interfaces for which there
is an Ada version (for the compiler) and a shadow version (for the
Examiner.)

1) Add the following to your Examiner index file:

interfaces spec is in interfaces.shs
spark_interfaces spec is in spark_interfaces.shs

2) interfaces.shs contains

package Interfaces
is
type Unsigned_32 is mod 2**32;
-- ... and similarly for other Unsigned_XX types
end Interfaces;

3) spark_interfaces.shs contains

with Interfaces;
--# inherit Interfaces;
package SPARK_Interfaces
is
function Rotate_Left_32
(Value  : Interfaces.Unsigned_32;
Amount : Natural) return Interfaces.Unsigned_32;

end SPARK_Interfaces;

(note this removes the overloading, and declares the function so it's
legal SPARK)

with Interfaces;
package SPARK_Interfaces
is
function Rotate_Left_32
(Value  : Interfaces.Unsigned_32;
Amount : Natural) return Interfaces.Unsigned_32 renames
Interfaces.Rotate_Left;

end SPARK_Interfaces;

(note this _renames_ the original function from Interfaces, so you
still
get the efficiency of the Intrinsic version.)

OK?
- Rod


 0
7/21/2009 9:31:32 AM
Rod Chapman wrote:
> OK - it's done as follows...

Looks good.

Thanks very much!

 0
xorquewasp (64)
7/21/2009 9:38:19 AM
xorque,
If it's not a dumb question: what exactly are you trying to
implement with SPARK?  It seems rather ambitious - you've
been pushing the boundaries a fair bit....
- Rod Chapman, SPARK Team

 0
7/21/2009 9:54:49 AM
Rod Chapman wrote:
> xorque,
>  If it's not a dumb question: what exactly are you trying to
> implement with SPARK?  It seems rather ambitious - you've
> been pushing the boundaries a fair bit....

Currently, a UTF-8 encoder/decoder.

Quite a few questions I've posted on here have been related
to "toy" projects testing what can be done sanely with this
degree of verification in Ada. I've rarely been disappointed.

I'm not currently writing anything that could be described
as "high-integrity" but I try to use SPARK wherever possible
as I do care deeply about software quality.

 0
xorquewasp (64)
7/21/2009 10:00:18 AM
xorque schrieb:

> I'm not currently writing anything that could be described
> as "high-integrity" but I try to use SPARK wherever possible
> as I do care deeply about software quality.

Can I second this?  In writing a double buffer properly,
in particular when varying length characters need to be
handled, SPARK is really helpful, if only to sort out
and document the author's assumptions, omissions, and errors.

Same for a live topsorted structure that is waiting on
my shelf to be finished.

 0
7/21/2009 10:40:29 AM
xorque a �crit :
> Rod Chapman wrote:
>> xorque,
>>  If it's not a dumb question: what exactly are you trying to
>> implement with SPARK?  It seems rather ambitious - you've
>> been pushing the boundaries a fair bit....
>
> Currently, a UTF-8 encoder/decoder.
>
FYI:
Rather than inventing your own interface, there is currently a proposal
for coding/decoding functions, see AI05-0137.

--
---------------------------------------------------------

 0
rosen (784)
7/21/2009 10:46:02 AM
> Rather than inventing your own interface, there is currently a proposal
> for coding/decoding functions, see AI05-0137.

Unfortunately, in it's current state, that interface isn't possible to
implement in SPARK directly (without a non-SPARK wrapper)
It uses exceptions, returns unconstrained arrays, etc.

 0
xorquewasp (64)
7/21/2009 11:33:47 AM

Similar Artilces:

what does SHIFT-left-or-right of up-down-left-right do?
Well, I know about shift up-and-down: shift-right ("red" or whatever) up and down on choose-box, HIST, things like that, take the cursor all the way to the beginning or the end. shift-left ("white") on up and down scroll the screen-full up or down (the FIRST such click *stupidly* goes to the final CURRENTLY-ON-SCREEN choice or whatever (meaning TWO double-button-pushes to scroll-down that FIRST time.) What are some of the OTHER possibilities, ie with the left and right arrows? Oh, apparantely undocumented, I've found (via mistaken key-pushes) that RIGHT-arrow will do a SWAP (on stack), and that an UP-arrow gets you into HIST (that HIST is *one nice feature*!) Other tricks with those arrows? Thanks! David David Combs wrote: > Well, I know about shift up-and-down: > > shift-right ("red" or whatever) up and down on > choose-box, HIST, things like that, take the > cursor all the way to the beginning or the end. > > shift-left ("white") on up and down scroll the > screen-full up or down (the FIRST such click > *stupidly* goes to the final CURRENTLY-ON-SCREEN > choice or whatever (meaning TWO double-button-pushes > to scroll-down that FIRST time.) > > > What are some of the OTHER possibilities, ie with the > left and right arrows? > > > Oh, apparantely undocumented,...

does PHP read left to right or right to left?
I've two functions. currentHeadline looks in $_GET for a variable called 'image' and prints what it finds. showThumbnail takes an image for a parameter and resizes it before sending it to the screen. But when I do this: <?php showThumbnail(currentImage(), 20, 20); ?> showThumbnail is telling me that it is not being given a file name, and currentImage is printing the file name to the screen. How is that possible? What is the right way to do this? lawrence k wrote: > I've two functions. currentHeadline looks in$_GET for a variable > called 'image' and pr...

How to shift Left or Right in SSE2
How do I do a bitwise shift left or right in SSE2? I would like that each of the 4 Word is shifted left (or right) by a number of n bits. I could only find _mm_srai_epi32 (only right!), which howevere does not do what I want, as it brings in introduce the sign bit. Thanks, Fabio spamtrap@crayne.org writes: > How do I do a bitwise shift left or right in SSE2? > > I would like that each of the 4 Word is shifted left (or right) by a > number of n bits. > > I could only find _mm_srai_epi32 (only right!), which howevere does > not do what I want, as it brings in int...

Changing x-axis plot from right to left to left to right
Hi, For mathematical reasons, I need to change the way that gnuplots my data along the X axis from right to left to left to right (that is, at the minute it plots from 20 down to 1, not from 1 to 20) I am aware of set xrange reverse but this just inverts the whole graph and displays from 17 .... 1 down along the x-axis rather than plotting the other way round. I'm rather stuck and would appreciate some advice. Regards Jamie On 14.08.2012 17:52, Jamie Rees wrote: > For mathematical reasons, I need to change the way that gnuplots my > data along the X axis from right to left to left to right (that is, > at the minute it plots from 20 down to 1, not from 1 to 20) That makes no sense whatsoever. gnuplot generates some kind of picture. It makes absolutely no difference whatsoever whether a line was drawn from left to right or right to left --- it'll be the same line in the end, consisisting of exactly the same pixels being coloured. So since this doesn't make sense, maybe you should tell us what your actual problem is, so we can find out how that might be solved. On Tuesday, August 14, 2012 6:12:33 PM UTC+1, Hans-Bernhard Br=F6ker wrote: > On 14.08.2012 17:52, Jamie Rees wrote: >=20 >=20 >=20 > > For mathematical reasons, I need to change the way that gnuplots my >=20 > > data along the X axis from right to left to left to right (that is, >=20 > > at the minute it plots from...

Text widget with mixed left-to-right and right-to-left Unicode text abilities?
Hi, is there one of these? If not I might have a go at writing a simple one of them.... Apologies if this is a FAQ, I did search the archive a bit before posting. Best, Charles. ...

Changing M-<right,left> to C-<right,left>
Hello, I tried to change the word moving behaviour as shown in the post title and could not. Part of my .emacs is below. (global-set-key (kbd "C-z") 'undo) (global-set-key (kbd "C-<right>") 'forward-word) (global-set-key (kbd "C-<left>") 'backward-word) Finally, how could I open a new buffer proportionally in the same window? For instance, if I open a new buffer with C-x 2 and then open the new buffer the window is split in two equal halves. I'd prefer to have it 70%, 30%. TIA, Andre Luiz AndreLTR <andreltramos@gmail.com> writes: > Hello, > > I tried to change the word moving behaviour as shown in the post title > and could not. Part of my .emacs is below. > > (global-set-key (kbd "C-z") 'undo) > (global-set-key (kbd "C-<right>") 'forward-word) > (global-set-key (kbd "C-<left>") 'backward-word) Works for me. Seems the code is not evaluated at all for you, dunno why, presumably something is wrong with your init file. > Finally, how could I open a new buffer proportionally in the same > window? For instance, if I open a new buffer with C-x 2 and then open > the new buffer the window is split in two equal halves. I'd prefer to > have it 70%, 30%. You can use the prefix arg of `split-window-below' to specify window heights in lines, see the doc string. Is that acceptable? ...

Using Ada (or SPARK) in Ada-unaware environment
Hi, Imagine a control system (to be developed) which needs to interact with some devices. Those devices are supplied with C drivers and libraries. What is the recommended practice for developing this control system in Ada (or SPARK)? I basically see two options for this: 1. Enjoy Ada's ability to interface with C libraries (pragma Import) and write everything in Ada. 2. Write separate programs in C (or C++) that will be responsible only for talking to the devices via their C access libraries. Write the main controller in Ada, as another separate program, and use some form of interprocess communication to have all those components talk. The advantage of the second option is that the controller part can be easily tested in isolation or in a fake environment. Are there some other options for this? What is the industry recommented practice? Regards, -- Maciej Sobczak : http://www.msobczak.com/ Programming : http://www.msobczak.com/prog/ Maciej Sobczak wrote: > Hi, > > Imagine a control system (to be developed) which needs to interact with > some devices. Those devices are supplied with C drivers and libraries. Been there a couple of times. > What is the recommended practice for developing this control system in > Ada (or SPARK)? I basically see two options for this: > > 1. Enjoy Ada's ability to interface with C libraries (pragma Import) and > write everything in Ada. I have always used this option. It works well *un...

how to locate right slot in a range with right-shifting and offset?
Hi all, Assume I non-uniformally break down a range from 0 to (2^10)-1 into (2^4)-1 blocks. |----|---|------|---|......|--| 0 5 7 (2^10)-1 For a given value x (x may be from 0 to 2^10-1), I would like to locate what block x should be in. For example if x is 6, I want to find the second block (from 5 to 7) in the above figure. ( x is integers). In a technical report, for this task, I see they use the operator: block_address=x >> shift_amount + offset_amount. (>> is right shift). where shift_amount and offset_amount are the same for all values of x. (all ...

Right or Left ?
A simple multimedia setup can be a display monitor with speakers positioned on both sides. Think of this equipment as being on a 'stage' in a theater, and the user as being the 'audience' in that theater. What is called the "left" speaker -- is it the one on the left of the audience (as viewed by the audience), or the one on the left of the stage (as viewed by an actor standing ON the stage, facing out towards the audience) ? mikus Sir: Mikus Grinbergs wrote: > A simple multimedia setup can be a display monitor with > speakers positioned on both sides. Think of this equipment > as being on a 'stage' in a theater, and the user as being the > 'audience' in that theater. > > What is called the "left" speaker -- is it the one on the left > of the audience (as viewed by the audience), or the one on the > left of the stage (as viewed by an actor standing ON the stage, > facing out towards the audience) ? > Left is audience left (stage right). You plug the left speakers into the jack marked left and let the recording studio worry about stage left or stage right. In computers, though, one has to make sure all the wires are plugged in correctly, and most home builders and factory assemblers don't care. Which is why digital transfer is important. An easy test is to turn off one side using a multimedia control like balance and seeing which speaker tal...

left shift operator behaves like left rotate when the operand is a variable.
Below is a snippet of code and the result (compiler version also mentioned). I fail to understand why the left shift operator behaves as if it were the left rotate operator when the operand is a variable. $cat test.c #include <stdio.h> int main(void) { unsigned int a = 32, b = 33; printf("with constants 1 << 32 = %u, 1 << 33 = %u\n", 1<<32, 1<<33); printf("with variables 1 << 32 = %u, 1 << 33 = %u\n", 1<<a, 1<<b); return 0; }$ gcc test.c test.c: In function 'main': test.c:6:5: warning: left shi...

t = (t->left != NULL) ? t->left : t->right;
hi i am learning C++ and when trying to implement a binary search tree for the first time I came across: t = (t->left != NULL) ? t->left : t->right; in a remove function, I have never seen this syntax and was wondering if anyonr could explain to me what it does. thanks in advance -joe [ See http://www.gotw.ca/resources/clcm.htm for info about ] [ comp.lang.c++.moderated. First time posters: Do this! ] it is the same as if ( t->left != NULL ) t = t->left; else t = t->right; Best regards, Alexey. [ See http://www.gotw.ca/resources/c...

Right-to-left languages?
Hi all, Can anyone please report the status of rendering of right-to-left languages in tk? I develop an LGPL NLP-related application (http://www.ellogon.org) and recently I got a question about supporting the Hebrew language. I need information on how the text widget can render these kind of languages and possible tkhtml. I feel a little akward for asking such a question :-) but I have no experence with right-to-left languages... Regards, George Hi Georgios, "Georgios Petasis" <petasis@iit.demokritos.gr> writes: > Can anyone please report the status of rendering of right-to-left > languages in tk? I develop an LGPL NLP-related application > (http://www.ellogon.org) and recently I got a question about > supporting the Hebrew language. Bidi is not supported on Tk yet. "Not supported" has different consequences depending on the widget and the underlying platform toolkit. For read-only widgets there are platform specific work-arounds and on some native controls (like menus on Windows and Mac OS X) it just works automatically. You may want to look into gnocl, the Tcl binding for the Gnome toolkit. Gnome is supposed to support bidi fine. I have never tried it myself though. benny Georgios Petasis wrote: > > Hi all, > > Can anyone please report the status of rendering of right-to-left > languages in tk? I develop an LGPL NLP-related application > (http://www.ellogon.org) and recently I got a question about s...

Left and Right arrows
Hi, In recently recieved some excellent advice which ebnabled me to make a form behave as a spreadsheet with respect to the down and up arrow keys. To develop this further I would like the right and left arrow to move to the next or previous tab control. DoCmd.GotoRecord,,AcNext does the business for down, but nowhere can I find a 'docmd go to next tab' or words to that effect!!! Any ideas? Hum, I assume when you say "tab", you are talking about a tab control? I would not take away the left/right arrow keys...as then how can a user edit data in a field? They need the arrow keys to move within that field. If the whole field is highlighted when the cursor enters..then you can normally use the left/right arrows to move to the next/previously control (is this what you are asking for now???). However, if a users is actually typing/editing data in a control..then they need the left right arrow keys for editing. I don't think it is a very good idea to steal those keys, as then how can a user edit text in a field? You can usually hit ctrl-TAB to jump to the next tab. Also, perhaps ctrl-right arrow, and ctrl-left arrow might be a possible keys to use..but I can't see stealing the left/right arrow keys. To steal the ctrl-right/ and left key, you can add the following code to your keydown handler: Dim intTabCount As Integer Const TabMax As Integer = 1 ' max number of tabs (less 1, since this is zero...

Right-to-left text
I come back to right-to-left text such as Arabic and Hebrew. (Previous thread was "non-Latin-1 in iCab 3".) My test page http://www.unics.uni-hannover.de/nhtcapri/right-to-left.html lists all HTML and CSS constructs for bidirectional text. It uses only ASCII digits! You do not need to know Arabic or Hebrew; you don't even need fonts with Arabic or Hebrew letters. If your browser passes this test, it is likely to display Arabic and Hebrew pages correctly. ...

Bitwise right shift
Hi all, I'm trying to write a program that extracts the first k bits of 64-bit double values, given 2^k (which I've defined as size). Here, I use the example that k = 3. For example, 101001...011 would return 5, since the first 3 bits are 101. #include <stdio.h> #include <math.h> #define size 8 #define NBITS 64 // number of bits in the datatype int main() { double var, nvar; unsigned int shift = 0; int k; var = pow(2, 63) + pow(2, 61); k = (int)log2(size); nvar = var>>(NBITS-k); printf("nvar = %lf\n", ...

shift right arithmetic
is there an equivalent way in verilog to do this: The contents of the low-order 32-bit word of a number are shifted right, duplicating the sign-bit (bit 31) in the emptied bits It's so easy that I'm not sure I understand your meaning right. @clk reg A[31:0]= {A[31],A[31:1]} "rekz" <aditya15417@gmail.com> ??????:ade3aa13-3209-4ba6-b534-87c624d542e8@x22g2000yqx.googlegroups.com... > is there an equivalent way in verilog to do this: > > The contents of the low-order 32-bit word of a number are shifted > right, duplicating the sign-bit (bit 31) in the emptied > bits rekz wrote: > is there an equivalent way in verilog to do this: > > The contents of the low-order 32-bit word of a number are shifted > right, duplicating the sign-bit (bit 31) in the emptied > bits Are you looking for the >>> operator? In reality there are many ways to do this. The >>> operator only works if the value is signed. For unsigned values you need to either cast it signed or resort to bit manipulation like the previous poster showed. Cary On Sun, 07 Mar 2010 23:54:35 -0800, "Cary R." wrote: >The >>> operator only works if the value is signed. WHOAH! How many times have I ranted about this...? Let's try again. ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ The >>> operator gives sign-extended shift only if it is used in a signed EXPRESSION....

Stick left AND right

Print shifted left
On all of my documents, the print is shifted about 1/8 to the left. I am Using Suse 9.2, an Epson 740 and an HP Deskjet 5740. The 740 uses the gimp-print driver and the 5740 uses the hpijs drivers. Since both printers, with different drivers were affected, and all printouts, I am thinking the problem may be with Ghostscript. Can anyone help in trouble shooting this? Any and all help appreciated. -- Rick Rick wrote: > On all of my documents, the print is shifted about 1/8 to the left. I > am Using Suse 9.2, an Epson 740 and an HP Deskjet 5740. The 740 uses > the gimp-print dri...

Why not automatic \left and \right ?
Hi folks, I've been wondering why \left and \right aren't assumed in the math mode. I thought it would be nice if \left and \right were automatic. I mean, I'd like all opening parens "(" to be regarded as "\left(" and closing parens as "\right)". It is rare (in my use) that automatic "\left(" or "\right)" would do any harm. When parens aren't paired, we could still use \left or \right: \left( something tall \right. If we ever need to suppress the stretching of parens, we could explicitly say something li...

Left or Right Function
Hi all, Is there in Matlab a function like the LEFT function in access that allows to define as a new variable the first (or last) N characters of a string or number? thanks "Cesare " <cesare_fracassi@yahoo.com> wrote in message <fbaf18$hu6$1@fred.mathworks.com>... > Hi all, > > Is there in Matlab a function like the LEFT function in > access that allows to define as a new variable the first (or > last) N characters of a string or number? > > thanks > I dont know about access, but try this: if ur variable is an String var='Characte...

Right to left packing
Hi, I have some right-to-left requirements: I need the text widget write text RTL, and I'd like some notebook widget (BWidget, Tix) have its tabs ordered right to left. Is this possible? Thanks On Mar 18, 12:05=A0pm, iu2 <isra...@elbit.co.il> wrote: > Hi, > > I have some right-to-left requirements: I need the text widget write > text RTL, and I'd like some notebook widget (BWidget, Tix) have its > tabs ordered right to left. > > Is this possible? "Possible" is a very interesting word. Take a look at http://wiki.tcl.tk/315= 8 where bidi rendering is discussed, and the author mentions a couple of projects he's done in tcl and tk to simulate things. On Mar 18, 6:30 pm, "Larry W. Virden" <lvir...@gmail.com> wrote: > On Mar 18, 12:05 pm, iu2 <isra...@elbit.co.il> wrote: > > > Hi, > > > I have some right-to-left requirements: I need the text widget write > > text RTL, and I'd like some notebook widget (BWidget, Tix) have its > > tabs ordered right to left. > > > Is this possible? > > "Possible" is a very interesting word. Take a look athttp://wiki.tcl.tk/3158 > where bidi rendering is discussed, and the author mentions a couple of > projects he's done in tcl and tk to simulate things. What I meant was not bidi text rendering but, rather, the look of widgets. For example, the tabs of a notebook arranged from right to left instead of...

Injected Right Shift
My application currently does keyboard injection and everything works... except for the right shift key. I don't know why, the other right-modifier keys all work but right shift key doesn't go through. MapVirtualKey returns 0 when I try to map 0x36 (the scancode for right shift) and if I manually set the wVk to VK_RSHIFT it ends up getting changed to 0 sometime before my low level keyboard hook captures it (the OS is removing the VK) but the scancode stays as 0x36. I have searched everywhere for an answer but have been unable to find anything. Does anyone know what the trick ...

Right to left tabularx?
Does anyone know if there is a way to make a tabular(x) table flip around- ie, so that the entries go from right to left- without simply redoing the table by hand? I'm doing a lot of tables in Arabic, and it is a pain to enter things that will be in a right to left table when I'm typing left to right in my text editor. Thanks! Alex ...

spacing after \right) and before \left)

Web resources about - SPARK left/right shift. - comp.lang.ada

Sparks - Wikipedia, the free encyclopedia
Text is available under the Creative Commons Attribution-ShareAlike License ;additional terms may apply. By using this site, you agree to the ...

Quit Facebook Day Fails To Spark Mass Exodus
Quit Facebook Day Fails To Spark Mass Exodus

Ms. Magazine - "Hobson sparks a discussion among other pop... - Facebook
"Hobson sparks a discussion among other pop culture critics about female empowerment, combining feminism and 'traditional' roles, and the 'politics ...

Abuse of Joel Thompson and family sparks security issue for Cronulla Sharks
A drunken fan abused Joel Thompson in front of his wife and two year old daughter, while there are concerns about fans invading the ground after ...

Foxtel price rise sparks backlash but boosts profit
Foxtel has raised its prices for the first time in two years, prompting a backlash on social media from some users but potentially boosting its ...

Anorexia is ‘self-indulgent’: TV presenter Joan Bakewell sparks outrage
A BRITISH television broadcaster has sparked outrage, after labelling anorexia as a sign of ‘narcissism’ in young people, and insisting the condition ...

Foxtel price rise sparks backlash but boosts profit
Foxtel has raised its prices for the first time in two years, prompting a backlash on social media from some users but potentially boosting its ...

Robot battle sparks female students' interest in STEM subjects
As Australia struggles to keep high school students interested in STEM subjects, a robot battle competition is catching their attention.

High Times, Sparks & Honey Team Up to Reposition Marijuana - Agency News - AdAge
Cannabis-focused media company High Times is collaborating with Omnicom Group agency Sparks & Honey to help tell the evolving story of marijuana ...

Foxtel price rise sparks backlash but boosts profit
Foxtel has raised its prices for the first time in two years, prompting a backlash on social media from some users but potentially boosting its ...

Resources last updated: 3/23/2016 3:13:46 AM