Skip to main content

It's a Bigger World than Java and C++

We hear a lot about Java and C++, but that doesn't mean they're the only languages developers are using.
Tokeneer was developed for the U.S. National Security Agency (NSA), an outfit known for keeping things secret. Which makes it even more surprising that not only did the NSA acknowledge Tokeneer's existence, but they released it as open source software.
In a nutshell, Tokeneer is a proof-of-concept of what's called "high-assurance software engineering." Secure software, in other words. Software you can trust. Software that must work correctly or else the consequences could be calamitous. And software that's written in Ada—yes, Ada—and developed using Praxis High Integrity Systems (www.praxis-his.com) Correctness-by-Construction (CbyC) methodology, the SPARK Ada language (www.sparkada.com), and AdaCore's GNAT Pro environment (www.adacore.com). The project demonstrates how to meet or exceed all those things that are necessary to achieve high assurance, such as Evaluation Assurance Level 5 in the Common Criteria (whatever that is). All in all, Tokeneer was created in just 260-person days, and implemented in about 10,000 lines of code. Originally a subset of the Ada language, SPARK Ada is designed in such a way that all SPARK programs are legal Ada programs.
No less than Tony Hoare, Fellow of the Royal Society of Microsoft Research, says that "the Tokeneer project is a milestone in the transfer of program verification technology into industrial application. Publication of the full documents for the project has provided unprecedented experimental material for yet further development of the technology by pure academic research. It will serve as a touchstone to chart and measure progress of the basic science of programming, on which the technology is based." Tokeneer is aimed at both the industrial and academic communities, forming an base for research in program verification and as a high-level teaching aid for educators. You can download the entire Tokeneer project, including requirements, security target, specifications, designs, source code, and proofs at www.adacore.com/home/gnatpro/tokeneer/.
Jonathan Erickson
Editor-in-Chief
jerickson@ddj.com
Read more on:
www.adacore.com/home/gnatpro/tokeneer/.
IntellaSys (www.intellasys.net) ,www.python.org,

Comments

Popular posts from this blog

Xilinx's Interview Questions

Xilinx is the world's one of largest supplier of programmable logic devices. It has started R & D department in Hyderabad, India. It has broad scope for embedded system programming in device driver in linux.

Before the interview you have to feel the Xilinx form with information containing all academic details, current/previous employer, contacts of employer( to check out info about you), current ctc, expected ctc and expected date of joining, etc.

I appeared two back to back technical interviews.

The first interview was taken by a young man look like just crossed 30's.

He asked me to tell me about myself.

Then he asked my experience.

He checked my expertise in resume.

He asked questions about RTOS, and Linux Device Drivers.
What is RTOS ? Define it.
How a linux device driver works?
How a character driver works?

He looked at my project summaries and started to ask in depth questions about each project.

After that he asked me to write to delete nth node from starting in Singly Linked Li…

Rajasthan Board 10th Results | rajedubord.nic.in | RBSE

Raj Board of Secondary Education, Rajasthan Results at rajeduboard.nic.inBoard of Secondary Education, Rajasthan Ajmer declared result of secondary examination today at 4PM official site is rajedubord.nic.in

check Secondary Examination- 2008 Result
(To be announced on July 1st, 2008 at 4:00 PM)
source
http://rajresults.nic.in/

Declared result
Praveshika Examination-2008 Result
(Announced on June 25, 2008 at 4:00 PM)

The history of the Board of Secondary Education Rajasthan (BSER) is a remarkable panorama of progressive record of the futurological vision for developing a dynamic system of various sub-systems of examinations and highlights of the academic excellence of the last four decades. The BSER took rapid strides for promotion and development of Secondary Education in Rajasthan, spread over 3,42,239 sq. km. and in more than 6000 schools located in 32 districts involving 8.5 lakhs students for Secondary and Senior Secondary Examination in the year 2000.

At present the Board is conducting …

Delete Last Char in String C program Simple Way

How to delete the last character in a string?
Lets say I have a string "/data/share/" I want to delete the last character from the string ie "/" so that output will be "/data/share"; Here are some methods to do this in C language.
one way could be use of strncat() function;
char*strncat(char*restricts1, constchar*restricts2, size_tn);
The strncat() function appends not more than n characters from s2, and
then adds a terminating `\0'.
#include
Another simple way is,
say the string variable is str_p
Then simply put
str_p[(strlen(str_p)-1)] = '\0';
And you are done;